[Merged by Bors] - chore(category_theory/monad): golf and lint monadic adjunctions #5769
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
I am happy to remove some nolints for you!
… functions (#5636) Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
### Changes in `order/filter/basic` * add `filter.inter_mem_sets_iff`; * rename `filter.Inter_mem_sets` to `filter.bInter_mem_sets`, make it an `iff` `[simp]` lemma; * add a version `filter.bInter_finset_mem_sets` with a protected alias `finset.Inter_mem_sets`; * rename `filter.sInter_mem_sets_of_finite` to `filter.sInter_mem_sets`, make it an `iff` `[simp]` lemma; * rename `filter.Inter_mem_sets_of_fintype` to `filter.Inter_mem_sets`, make it an `iff` `[simp]` lemma * add `eventually` versions of the `*Inter_mem_sets` lemmas. ### New `@[mono]` attributes * `set.union_subset_union` and `set.inter_subset_inter` instead of `monotone_union` and `monotone_inter`; `mono*` failed to make a progress with `s ∩ t ⊆ s' ∩ t'` goal. * `set.image2_subset` * `closure_mono`
…complete lattices (#5575) Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: Oliver Nash <github@olivernash.org>
…ble (#5687) An irreducible polynomial is nonzero, so this hypothesis is unnecessary.
…here (#5647) * use `ae_measurable f (μ.restrict s)` in more lemmas; * introduce `measurable_at_filter` and use it.
define sigma_compact_space update module doc for topology/subset_properties define shearing some lemmas in set.basic, equiv.mul_add and topology.instances.ennreal Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
… even/odd lemmas (#5404) Complex (and some real) trigonometry lemmas, parity propositions, and some field algebra.
I am happy to remove some nolints for you!
Restrict an alg_hom or alg_equiv to an is_splitting_field.
I am happy to remove some nolints for you!
…r limits (#5674) - Show that the forgetful functor `over X => C` creates colimits, generalising what was already there - Golf the proofs using this new instance - Add module doc and duals of the above
…dule structure (#5667) These were added originally so that `semimodule'` was lower priority than `semimodule`, as the `semimodule'` instance took too long to resolve. However, this happens automatically anyway, since the former appears before the latter - the simple existence of the `semimodule` shortcut instances was enough to solve the long typeclass-resolution paths, their priority was a red herring. The only effect of these attributes was to cause these instances to not take priority over `add_comm_monoid.nat_semimodule`, which was neither intended nor desirable.
As mentioned here: #5516 (comment) The linter is giving new errors, so I might as well fix them in this PR.
Add two strict subset lemmas for Icc, discussed in https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Icc_ssubset_Icc. Co-authored-by: Damiano Testa
…measure (#5688) * generalize `outer_measure.exists_is_measurable_superset_of_trim_eq_zero` to `outer_measure.exists_is_measurable_superset_eq_trim`; * generalize `exists_is_measurable_superset_of_null` to `exists_is_measurable_superset`; * define `to_measurable mu s` to be a measurable superset `t ⊇ s` with `μ t = μ s`; * prove `countable_cover_nhds`: in a `second_countable_topology`, if `f` sends each point `x` to a neighborhood of `x`, then some countable subfamily of neighborhoods `f x` cover the whole space. * `sigma_finite_of_countable` no longer assumes that all sets `s ∈ S` are measurable.
Note that unlike `linear_map`, `range` cannot return a submodule, only a `sub_mul_action`. We also can't guarantee closure under `smul` unless the map has at least one argument, as there is nothing requiring the multilinear map of no arguments to be zero.
Updates to `undergrad.yaml` (including reverting some changes from #5638, after further discussion), and fix a docstring typo in `measure_theory.interval_integral`.
this lemma was pretty slow, now it is pretty fast
…e 67 (#5709) This saves us a lot of `()` In particular, lean no longer thinks that `∑' i, f i = 37` is a tsum of propositions.
- adds Witt vectors - adds perfection of a ring - deduplicates Zariski topology - moves some items to a new subsection "Number theory" Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
This occurs because when we name the atoms in `A * B = 2`, `A` is the first and `B` is the second, and once we put it in horner form it ends up as `B * A = 2`; but then when we go to rewrite it again `B` is named atom number 1 and `A` is atom number 2, so we write it the other way around and end up back at `A * B = 2`. The solution implemented here is to retain the atom map across calls to `ring.eval` while simp is driving it, so we end up rewriting it to `B * A = 2` in the first place but in the second pass we still think `B` is the second atom so we stick with the `B * A` order. Fixes #2672
…tices (#5493) Provides possible instances of `bounded_distrib_lattice`, `boolean_algebra`, `complete_lattice`, and `complete_boolean_algebra` on a simple lattice Relates the `is_atom` and `is_coatom` conditions to `is_simple_lattice` structures on intervals Shows that all three conditions are preserved by `order_iso`s Adds more instances on `bool`, including `is_simple_lattice` Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…ⁿ)` (#5756) ### Lemmas about analytic functions * add `has_fpower_series_on_ball.uniform_geometric_approx'`, a more precise version of `has_fpower_series_on_ball.uniform_geometric_approx`; * add `has_fpower_series_at.is_O_sub_partial_sum_pow`, a version of the Taylor formula for an analytic function; ### Lemmas about `homeomorph` and topological groups * add `simp` lemmas `homeomorph.coe_mul_left` and `homeomorph.mul_left_symm`; * add `map_mul_left_nhds` and `map_mul_left_nhds_one`; * add `homeomorph.to_equiv_injective` and `homeomorph.ext`; ### Lemmas about `is_O`/`is_o` * add `simp` lemmas `asymptotics.is_O_with_map`, `asymptotics.is_O_map`, and `asymptotics.is_o_map`; * add `asymptotics.is_o_norm_pow_norm_pow` and `asymptotics.is_o_norm_pow_id`; ### Misc changes * rename `div_le_iff_of_nonneg_of_le` to `div_le_of_nonneg_of_le_mul`; * add `continuous_linear_map.op_norm_le_of_nhds_zero`; * golf some proofs.
b-mehta
added
the
awaiting-review
github-actions
bot
added
the
blocked-by-other-PR
1 task
github-actions
bot
removed
the
blocked-by-other-PR
|
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
jcommelin
approved these changes
Jan 16, 2021
jcommelin
added
awaiting-author
b-mehta
added
awaiting-review
github-actions
bot
added
the
merge-conflict
github-actions
bot
removed
the
merge-conflict
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Jan 18, 2021
Some lintfixes and proof golfing using newer API Co-authored-by: Oliver Nash <oliver.nash@gmail.com> Co-authored-by: leanprover-community-bot <leanprover.community@gmail.com> Co-authored-by: Yakov Pechersky <ffxen158@gmail.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: tb65536 <tb65536@uw.edu> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Mohamed Al-Fahim <malfahim8@gmail.com> Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Mario Carneiro <di.gama@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Some lintfixes and proof golfing using newer API