[Merged by Bors] - feat(topology/subset_properties): compact discrete spaces are finite #6191
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
From `lean-liquid`
Requested by @jcommelin. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
…minators in evaluating a polynomial (#6122) Evaluating a polynomial with integer coefficients at a rational number and clearing denominators, yields a number greater than or equal to one. The target can be any `linear_ordered_field K`. The assumption on `K` could be weakened to `linear_ordered_comm_ring` assuming that the image of the denominator is invertible in `K`. Reference: Liouville PR #4301.
There are three families of these for consistency with how we have three families of `is_scalar_tower` instances.
…ero (#6151) lemma eq_zero_iff_abs_lt_one
…)?` (#6153) This PR contains a couple of `simp` lemmas for `reindex` and its bundled equivs. Namely, it adds `reindex_refl` (reindexing along the identity map is the identity), and `reindex_apply` (the same as `coe_reindex`, but no `λ i j` on the RHS, which makes it more useful for `rw`'ing.) The previous `reindex_apply` is renamed `coe_reindex` for disambiguation.
…n and forgetful functor (#6154) Abelianization has been defined in `group_theory/abelianization` without realising it in category theory. This PR adds this feature. Furthermore, a module doc for abelianization is added and the one for adjunctions is expanded. Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>
…6159) 4X smaller proof term, elaboration 800ms -> 50ms Co-authors: `lean-gptf`, Stanislas Polu Note: supplying `coeff_pow_p f n` also works but takes 500ms to elaborate Co-authored-by: Jesse Michael Han <39395247+jesse-michael-han@users.noreply.github.com>
... of `bUnion_filter_eq_of_maps_to` looks nicer, slightly faster elaboration, 13% smaller proof term Co-authors: `lean-gptf`, Stanislas Polu Co-authored-by: Jesse Michael Han <39395247+jesse-michael-han@users.noreply.github.com>
… group (#5672) Adds a lemma stating that if top=bot in the subalgebra type then top=bot in the subgroup type. Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…r series (#5854) If a formal multilinear series has a positive radius of convergence, then its inverse also does.
… Dickson polynomials (#5869) and replace lambdashev with dickson 1 1. Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Julian <kuelsha@mathematik.uni-stuttgart.de>
…e is complemented iff atomistic (#6071) Shows that a compactly-generated modular lattice is complemented iff it is atomistic Proves extra lemmas about atomistic or compactly-generated lattices Proves extra lemmas about `complete_lattice.independent` Fix the name of `is_modular_lattice.sup_inf_sup_assoc` Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net>
…s theorem and related theorems (#6082) Move `submodule.singleton_span_is_compact_element` and `submodule.is_compactly_generated` to more appropriate locations. Add trivial order isomorphisms and order-iso lemmas. Show that `is_atomic` and `is_coatomic` are respected by order isomorphisms. Greatly simplify `is_noetherian_iff_well_founded`. Provide an `is_coatomic` instance on the ideal lattice of a ring and simplify `ideal.exists_le_maximal`.
…produce an element of the set (#6103)
…lean` (#6104) I was having trouble with circular imports related to `power_basis.lean`, so I decided to reshuffle some definitions to make `power_basis.lean` have less dependencies. That way, something depending on `power_basis` doesn't also need to depend on `intermediate_field.adjoin`. The following (main) declarations are moved: - `algebra.adjoin`: from `ring_theory/adjoin.lean` to `ring_theory/adjoin/basic.lean` (renamed file) - `algebra.adjoin.power_basis`: from `ring_theory/power_basis.lean` to `ring_theory/adjoin/power_basis.lean` (new file) - `adjoin_root.power_basis`: from `ring_theory/power_basis.lean` to `ring_theory/adjoin_root.lean` - `intermediate_field.adjoin.power_basis`: from `ring_theory/power_basis.lean` to `field_theory/adjoin.lean` - `is_scalar_tower.polynomial`: from `ring_theory/algebra_tower.lean` to `ring_theory/polynomial/tower.lean` (new file) The following results are new: - `is_integral.linear_independent_pow` and `is_integral.mem_span_pow`: generalize `algebra.adjoin.linear_independent_power_basis` and `algebra.adjoin.mem_span_power_basis`.
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
…s.lean file (#6161) split the file subset_properties.lean into another file called connected.lean which contains the properties that relate to connectivity. This is in preparation for a future PR proving properties about the quotient of a space by its connected components and it would add roughly 300 lines.
I am happy to remove some nolints for you!
…ults (#6127) This PR contains some changes to the lemmas involving `is_basis.to_matrix`, allowing the bases involved to differ in their index type. Although you can prove there exists an `equiv` between those types, it's easier to not have to transport along that equiv. The PR also generalizes `linear_map.to_matrix_id` to a form with two different bases, `linear_map.to_matrix_id_eq_basis_to_matrix`. Marking the second as `simp` means the first can be proved automatically, hence the removal of `simp` on that one.
From `lean-liquid`
`\\` in source code is converted to `\` in the generated html file, so one should have `\\\\` to generate proper line break for mathjax.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
… `set.is_wf` (#6113) Defines a predicate for when a set within an ordered type is well-founded (`set.is_wf`) Proves basic lemmas about well-founded sets
…g field of composition (#6148) Defines the surjective restriction map from the splitting field of a composition Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
… of submonoids/subgroups and their join (#6165) If `H` and `K` are subgroups/submonoids then `H ⊔ K = closure (H * K)`, where `H * K` is the pointwise set product. When `H` or `K` is a normal subgroup, it is proved that `(↑(H ⊔ K) : set G) = H * K`. <!-- put comments you want to keep out of the PR commit here. If this PR depends on other PRs, please list them below this comment, using the following format: - [ ] depends on: #abc [optional extra text] - [ ] depends on: #xyz [optional extra text] -->
… are (#6172) Add single lemma one_le_mul_of_one_le_of_one_le The lemma is stated for an `ordered_semiring`, but only multiplication is used. There does not seem to be an `ordered_monoid` class where this lemma would fit. Relevant Zulip chat: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/ordered_monoid.3F
Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>
… `lie_algebra.equiv` --> `lie_equiv` (#6179) Also renaming the field `map_lie` to `map_lie'` in both `lie_algebra.morphism` and `lie_module_hom` for consistency with the pattern elsewhere in Mathlib.
…ace; use `ring` instead (#6181) The `old_structure_cmd` change to `lie_algebra.is_simple` is unrelated and is included here only for convenience. `ring_commutator.commutator` -> `ring.lie_def`
jcommelin
added
the
awaiting-review
github-actions
bot
added
the
blocked-by-other-PR
Closed
1 task
|
Something seems to be wrong with the commit history? |
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! |
github-actions
bot
added
the
merge-conflict
github-actions
bot
removed
the
merge-conflict
|
Yeah, I messed up a |
sgouezel
reviewed
Feb 12, 2021
There was a problem hiding this comment.
The statement finite_of_is_compact_of_discrete is not really satisfactory, as it should be: take a discrete compact subset of any separated topological space. Then it is finite. But since we haven't got is_discrete yet, let's merge this version for now.
bors r+
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Feb 12, 2021
…6191) From `lean-liquid` Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: damiano <adomani@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yakov Pechersky <ffxen158@gmail.com> Co-authored-by: Anne Baanen <vierkantor@vierkantor.com> Co-authored-by: Julian-Kuelshammer <julian.kuelshammer@math.uu.se> Co-authored-by: Jesse Michael Han <hyrodi@gmail.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: tb65536 <tb65536@uw.edu> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Aaron Anderson <awainverse@gmail.com> Co-authored-by: Chase Meadors <c.ed.mead@gmail.com> Co-authored-by: Oliver Nash <github@olivernash.org> Co-authored-by: Calle Sönne <calle.sonne@gmail.com> Co-authored-by: leanprover-community-bot <leanprover.community@gmail.com> Co-authored-by: Adrián Doña Mateo <drnaia100@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
b-mehta
pushed a commit
that referenced
this pull request
Apr 2, 2021
…6191) From `lean-liquid` Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: damiano <adomani@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yakov Pechersky <ffxen158@gmail.com> Co-authored-by: Anne Baanen <vierkantor@vierkantor.com> Co-authored-by: Julian-Kuelshammer <julian.kuelshammer@math.uu.se> Co-authored-by: Jesse Michael Han <hyrodi@gmail.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: tb65536 <tb65536@uw.edu> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Aaron Anderson <awainverse@gmail.com> Co-authored-by: Chase Meadors <c.ed.mead@gmail.com> Co-authored-by: Oliver Nash <github@olivernash.org> Co-authored-by: Calle Sönne <calle.sonne@gmail.com> Co-authored-by: leanprover-community-bot <leanprover.community@gmail.com> Co-authored-by: Adrián Doña Mateo <drnaia100@gmail.com>
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.
From
lean-liquid