[Merged by Bors] - feat: define semisimple linear endomorphisms #9825
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
ocfnash
added
WIP
ocfnash
added
awaiting-review
|
✌️ ocfnash can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
This was part of a CR suggestion but I believe was unintentional.
|
bors merge |
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
winstonyin
added a commit
that referenced
this pull request
Jan 30, 2024
commit 4fcf5bd Author: Scott Morrison <scott@tqft.net> Date: Tue Jan 30 04:00:55 2024 +0000 chore: bump Std to leanprover-community/batteries#566 (#10117) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> commit 99afa84 Author: Yury G. Kudryashov <urkud@urkud.name> Date: Tue Jan 30 02:26:17 2024 +0000 feat(Logic/Embedding): add a lemma (#10096) * Make `Function.Embedding.setValue_eq` a `simp` lemma. * Add `Function.Embedding.setValue_eq_iff`. commit 41e0da3 Author: David Renshaw <dwrenshaw@gmail.com> Date: Tue Jan 30 02:26:16 2024 +0000 fix: use getTransparency in librarySearch SolveByElim.Config (#10052) commit 9cc09f6 Author: Yury G. Kudryashov <urkud@urkud.name> Date: Tue Jan 30 02:26:15 2024 +0000 chore(WithTop): less abuse of defeq to `Option _` (#9986) Also reuse proofs here and there. commit 15e555e Author: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Date: Tue Jan 30 02:26:14 2024 +0000 feat: characterize "eventually" in a subtype (#7568) Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com> Co-authored-by: ADedecker <anatolededecker@gmail.com> commit d3a6c9f Author: Scott Morrison <scott@tqft.net> Date: Tue Jan 30 01:07:06 2024 +0000 chore: bump Std to leanprover-community/batteries#242 (#10104) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> commit 132e511 Author: Winston Yin <winstonyin@gmail.com> Date: Tue Jan 30 00:03:21 2024 +0000 feat: Integral curves are either injective or periodic (#9343) Integral curves are either injective, constant, or periodic and non-constant. When we have notions of submanifolds, this'll be useful for showing that the image of an integral curve is a submanifold. - [x] depends on: #8886 Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de> commit b4d01dc Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Mon Jan 29 21:32:09 2024 +0000 refactor(MeasureTheory/Function/L1Space): rm two porting notes (#10056) Co-authored-by: Moritz Firsching <firsching@google.com> commit 7458f0e Author: Yury G. Kudryashov <urkud@urkud.name> Date: Mon Jan 29 18:36:04 2024 +0000 feat(Topology/Separation): define R₁ spaces, review API (#10085) - Define `R1Space`, a.k.a. preregular space. - Drop `T2OrLocallyCompactRegularSpace`. - Generalize all existing theorems about `T2OrLocallyCompactRegularSpace` to `R1Space`. - Drop the `[T2OrLocallyCompactRegularSpace _]` assumption if the space is known to be regular for other reason (e.g., because it's a topological group). - `Specializes.not_disjoint`: if `x ⤳ y`, then `𝓝 x` and `𝓝 y` aren't disjoint; - `specializes_iff_not_disjoint`, `Specializes.inseparable`, `disjoint_nhds_nhds_iff_not_inseparable`, `r1Space_iff_inseparable_or_disjoint_nhds`: basic API about `R1Space`s; - `Inducing.r1Space`, `R1Space.induced`, `R1Space.sInf`, `R1Space.iInf`, `R1Space.inf`, instances for `Subtype _`, `X × Y`, and `∀ i, X i`: basic instances for `R1Space`; - `IsCompact.mem_closure_iff_exists_inseparable`, `IsCompact.closure_eq_biUnion_inseparable`: characterizations of the closure of a compact set in a preregular space; - `Inseparable.mem_measurableSet_iff`: topologically inseparable points can't be separated by a Borel measurable set; - `IsCompact.closure_subset_measurableSet`, `IsCompact.measure_closure`: in a preregular space, a measurable superset of a compact set includes its closure as well; as a corollary, `closure K` has the same measure as `K`. - `exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds`: an auxiliary lemma extracted from a `LocallyCompactPair` instance; - `IsCompact.isCompact_isClosed_basis_nhds`: if `x` admits a compact neighborhood, then it admits a basis of compact closed neighborhoods; in particular, a weakly locally compact preregular space is a locally compact regular space; - `isCompact_isClosed_basis_nhds`: a version of the previous theorem for weakly locally compact spaces; - `exists_mem_nhds_isCompact_isClosed`: in a locally compact regular space, each point admits a compact closed neighborhood. Some theorems about topological groups are true for any (pre)regular space, so we deprecate the special cases. - `exists_isCompact_isClosed_subset_isCompact_nhds_one`: use new `IsCompact.isCompact_isClosed_basis_nhds` instead; - `instLocallyCompactSpaceOfWeaklyOfGroup`, `instLocallyCompactSpaceOfWeaklyOfAddGroup`: are now implied by `WeaklyLocallyCompactSpace.locallyCompactSpace`; - `local_isCompact_isClosed_nhds_of_group`, `local_isCompact_isClosed_nhds_of_addGroup`: use `isCompact_isClosed_basis_nhds` instead; - `exists_isCompact_isClosed_nhds_one`, `exists_isCompact_isClosed_nhds_zero`: use `exists_mem_nhds_isCompact_isClosed` instead. For each renamed theorem, the old theorem is redefined as a deprecated alias. - `isOpen_setOf_disjoint_nhds_nhds`: moved to `Constructions`; - `isCompact_closure_of_subset_compact` -> `IsCompact.closure_of_subset`; - `IsCompact.measure_eq_infi_isOpen` -> `IsCompact.measure_eq_iInf_isOpen`; - `exists_compact_superset_iff` -> `exists_isCompact_superset_iff`; - `separatedNhds_of_isCompact_isCompact_isClosed` -> `SeparatedNhds.of_isCompact_isCompact_isClosed`; - `separatedNhds_of_isCompact_isCompact` -> `SeparatedNhds.of_isCompact_isCompact`; - `separatedNhds_of_finset_finset` -> `SeparatedNhds.of_finset_finset`; - `point_disjoint_finset_opens_of_t2` -> `SeparatedNhds.of_singleton_finset`; - `separatedNhds_of_isCompact_isClosed` -> `SeparatedNhds.of_isCompact_isClosed`; - `exists_open_superset_and_isCompact_closure` -> `exists_isOpen_superset_and_isCompact_closure`; - `exists_open_with_compact_closure` -> `exists_isOpen_mem_isCompact_closure`; commit 7afbac6 Author: grunweg <rothgami@math.hu-berlin.de> Date: Mon Jan 29 17:52:04 2024 +0000 chore(Topology/PartialHomeomorph): rename type variables (#9632) Greek letters are dead, long live X, Y and Z. Same procedure as in previous renames. commit d883f18 Author: s1m7u <z5476255@ad.unsw.edu.au> Date: Mon Jan 29 16:54:51 2024 +0000 chore(Data/List/Rotate): add `@[simp]` to `rotate_replicate` (#10106) commit 89f9777 Author: Scott Morrison <scott@tqft.net> Date: Mon Jan 29 15:34:18 2024 +0000 chore: fix Punit->PUnit in CommMon_ (#10089) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> commit 00b71ef Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Mon Jan 29 14:47:04 2024 +0000 refactor(Probability/Kernel/CondCdf): mv tendsto_of_antitone (#10046) Co-authored-by: Moritz Firsching <firsching@google.com> commit 68c771a Author: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon Jan 29 13:56:07 2024 +0000 doc: fix typos (#10100) Fix minor typos in the following files: - [x] `Mathlib/GroupTheory/GroupAction/Opposite.lean` - [x] `Mathlib/Init/Control/Lawful.lean` - [x] `Mathlib/ModelTheory/ElementarySubstructures.lean` - [x] `Mathlib/Algebra/Group/Defs.lean` - [x] `Mathlib/Algebra/Group/WithOne/Basic.lean` - [x] `Mathlib/Data/Int/Cast/Defs.lean` - [x] `Mathlib/LinearAlgebra/Dimension/Basic.lean` - [x] `Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean` - [x] `Mathlib/Algebra/Star/StarAlgHom.lean` - [x] `Mathlib/AlgebraicTopology/SimplexCategory.lean` - [x] `Mathlib/CategoryTheory/Abelian/Homology.lean` - [x] `Mathlib/CategoryTheory/Sites/Grothendieck.lean` - [x] `Mathlib/RingTheory/IsTensorProduct.lean` - [x] `Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean` - [x] `Mathlib/AlgebraicTopology/ExtraDegeneracy.lean` - [x] `Mathlib/AlgebraicTopology/Nerve.lean` - [x] `Mathlib/AlgebraicTopology/SplitSimplicialObject.lean` - [x] `Mathlib/Analysis/ConstantSpeed.lean` - [x] `Mathlib/Analysis/Convolution.lean` commit e463fbf Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Mon Jan 29 13:15:22 2024 +0000 chore(Analysis/SpecialFunctions/JapaneseBracket): restore measurability (#10054) Co-authored-by: Moritz Firsching <firsching@google.com> commit cea4f7a Author: Scott Morrison <scott@tqft.net> Date: Mon Jan 29 10:59:18 2024 +0000 chore: cleanup some Yoneda lemma proofs (#10092) While thinking about simp lemmas for opposite categories (for the sake of comonoid objects, for the sake of group objects, for the sake of reductive groups), noticed some of the Yoneda lemma proofs can be golfed. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> commit 197378a Author: Adam Topaz <github@adamtopaz.com> Date: Mon Jan 29 10:12:33 2024 +0000 chore: Fix some porting notes and make some defs computable again. (#10062) These are some auxiliary definitions for the monoidal structure on a category induced by binary products and terminal objects. commit 86ffe04 Author: Yury G. Kudryashov <urkud@urkud.name> Date: Mon Jan 29 07:53:36 2024 +0000 chore(Order/Filter/ListTraverse): move from `Basic` (#10048) commit a4c1d9d Author: sgouezel <sebastien.gouezel@univ-rennes1.fr> Date: Mon Jan 29 07:53:35 2024 +0000 chore: split file on series of functions into two files (#9906) Currently, the same file contains the facts that series of functions are continuous (resp. smooth) under suitable assumption. I will need the result on continuity in a file of more topological nature. To avoid importing all calculus in this file, this PR splits the file `Analysis.Calculus.Series` into `Analysis.Calculus.SmoothSeries` and `Analysis.NormedSpace.FunctionSeries`. It's purely a splitting PR, no result added or removed. commit 1fa9ebf Author: Yury G. Kudryashov <urkud@urkud.name> Date: Mon Jan 29 06:37:18 2024 +0000 feat(Algebra/InfiniteSum): drop `[T2Space _]` assumption (#10060) * Add `CanLift` instance for `Function.Embedding`. * Assume `Injective i` instead of an equivalent condition in `hasSum_iff_hasSum_of_ne_zero_bij`. * Add `tsum_eq_sum'`, a version of `tsum_eq_sum` that explicitly mentions `support f`. * Add `Function.Injective.tsum_eq`, use it to drop `[T2Space _]` assumption in - `Equiv.tsum_eq`; - `tsum_subtype_eq_of_support_subset`; - `tsum_subtype_support`; - `tsum_subtype`; - `tsum_univ`; - `tsum_image`; - `tsum_range`; - `tsum_setElem_eq_tsum_setElem_diff`; - `tsum_eq_tsum_diff_singleton`; - `tsum_eq_tsum_of_ne_zero_bij`; - `Equiv.tsum_eq_tsum_of_support`; - `tsum_extend_zero`; * Golf some proofs. * Drop `Equiv.Set.prod_singleton_left` and `Equiv.Set.prod_singleton_right` added in #10038. @MichaelStollBayreuth, if you need these `Equiv`s, then please - restore them in `Logic/Equiv/Set`, not in `Data/Set/Prod`; - call them `Equiv.Set.singletonProd` and `Equiv.Set.prodSingleton`, following the `lowerCamelCase` naming convention for `def`s; - reuse the existing `Equiv.Set.prod` and `Equiv.prodUnique`/`Equiv.uniqueProd` in the definitions. commit 1da1e9e Author: sgouezel <sebastien.gouezel@univ-rennes1.fr> Date: Mon Jan 29 06:37:17 2024 +0000 feat: minor topological improvements (#9908) * Prove that a set is a Gdelta if and only if it is an intersection of open sets indexed by `ℕ`. * Cleanup porting todos in the Gdelta file * Rename `cluster_point_of_compact` to `exists_clusterPt_of_compactSpace ` * Generalize the class `T2Space` to `T2OrLocallyCompactRegularSpace` in the file `Support.lean` commit 4e0ccc0 Author: technosentience <28826901+technosentience@users.noreply.github.com> Date: Mon Jan 29 05:23:46 2024 +0000 feat(Data/Fin/Tuple/Basic): `repeat_comp_rev` (#9845) Prove `repeat_comp_rev`. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> commit f5a69ea Author: Kevin Buzzard <k.buzzard@imperial.ac.uk> Date: Mon Jan 29 01:14:44 2024 +0000 docs(Algebra/Algebra/Basic): get the type right (#10055) commit 995b1af Author: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon Jan 29 00:09:08 2024 +0000 doc(Mathlib/Algebra): fix typos (#10080) Fix minor typos in the `Mathlib/Algebra/CovariantAndContravariant.lean` file. commit c38c032 Author: Yury G. Kudryashov <urkud@urkud.name> Date: Sun Jan 28 23:24:42 2024 +0000 feat(Convex/Gauge): add `continuousAt_gauge` (#9911) commit 9f35a08 Author: Oliver Nash <github@olivernash.org> Date: Sun Jan 28 15:34:44 2024 +0000 feat: add lemmas `nullMeasurableSet_lt'` and `nullMeasurableSet_le` (#10074) Prior to this commit the state of Mathlib was: ```lean import Mathlib ``` Co-authored-by: teorth <tao@math.ucla.edu> commit e975e78 Author: Yury G. Kudryashov <urkud@urkud.name> Date: Sun Jan 28 14:42:17 2024 +0000 chore(Topology): fix a typo (#10070) There is no `NeBot` in this lemma commit 19b5ded Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Sun Jan 28 09:50:58 2024 +0000 refactor(Probability/Kernel/CondCdf): mv some theorems (#10036) Co-authored-by: Moritz Firsching <firsching@google.com> commit e8bfb67 Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Sun Jan 28 09:07:45 2024 +0000 refactor(Probability/Kernel/CondCdf): mv ofReal_cinfi (#10044) Co-authored-by: Moritz Firsching <firsching@google.com> commit d5277c9 Author: Matthew Robert Ballard <matt@mrb.email> Date: Sun Jan 28 02:42:13 2024 +0000 perf(NormedSpace/OperatorNorm): fix `simp` call and clean up porting notes (#9658) We clean up some porting notes and speed up this file. commit 09b44c1 Author: Christopher Hoskin <christopher.hoskin@gmail.com> Date: Sat Jan 27 19:32:54 2024 +0000 feat(GroupTheory/GroupAction/Group): invOf smul lemmas (#9972) Give `smul` versions of some existing `mul` lemmas: - `invOf_smul_smul` - smul_invOf_smul (c.f. mul_invOf_self_assoc) - `invOf_smul_eq_iff` (c.f. `invOf_mul_eq_iff_eq_mul_left`) (required for #7569) - `smul_eq_iff_eq_invOf_smul` (c.f `mul_left_eq_iff_eq_invOf_mul`) Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com> Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com> commit e4e10f9 Author: Michael Stoll <Michael.Stoll@uni-bayreuth.de> Date: Sat Jan 27 17:46:59 2024 +0000 feat(Topology/Algebra/InfiniteSum/Basic): add some lemmas on `tsum`s (#10038) This is the fifth PR in a sequence that adds auxiliary lemmas from the [EulerProducts](https://github.com/MichaelStollBayreuth/EulerProducts) project to Mathlib. It adds three lemmas on `tsum`s: ```lean lemma HasSum.tsum_fiberwise {α β γ : Type*} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [T2Space α] [RegularSpace α] [CompleteSpace α] {f : β → α} {a : α} (hf : HasSum f a) (g : β → γ) : HasSum (fun c : γ ↦ ∑' b : g ⁻¹' {c}, f b) a lemma tsum_setProd_singleton_left {α β γ : Type*} [AddCommMonoid γ] [TopologicalSpace γ] [T2Space γ] (a : α) (t : Set β) (f : α × β → γ) : (∑' x : {a} ×ˢ t, f x) = ∑' b : t, f (a, b) lemma tsum_setProd_singleton_right {α β γ : Type*} [AddCommMonoid γ] [TopologicalSpace γ] [T2Space γ] (s : Set α) (b : β) (f : α × β → γ) : (∑' x : s ×ˢ {b}, f x) = ∑' a : s, f (a, b) ``` and the necessary equivalences ```lean def prod_singleton_left {α β : Type*} (a : α) (t : Set β) : ↑({a} ×ˢ t) ≃ ↑t def prod_singleton_right {α β : Type*} (s : Set α) (b : β) : ↑(s ×ˢ {b}) ≃ ↑s ``` commit 0bcd6be Author: grunweg <rothgami@math.hu-berlin.de> Date: Sat Jan 27 17:21:40 2024 +0000 feat: two lemmas about cut-off functions (#9873) From sphere-eversion; I'm just upstreaming this. The version in sphere-eversion uses an unbundled design; we provide a bundled version (for now) to match the remaining file. Co-authored-by: grunweg <grunweg@posteo.de> commit f1919fd Author: Yuma Mizuno <mizuno.y.aj@gmail.com> Date: Sat Jan 27 14:51:46 2024 +0000 feat(CategoryTheory/Monoidal): add lemmas for the whiskerings (#9995) Extracted from #6307. commit c6cc35e Author: Christian Merten <christian@merten.dev> Date: Sat Jan 27 11:43:29 2024 +0000 docs(TensorProduct/Tower): fix doc string of `AlgebraTensorModule.assoc` (#10051) Matches variable names in the doc string with the variables used in the type signature of `AlgebraTensorModule.assoc`. commit ae8f621 Author: grunweg <rothgami@math.hu-berlin.de> Date: Sat Jan 27 11:43:28 2024 +0000 feat: four small lemmas about extended charts (#10001) From sphere-eversion; I'm just submitting them. commit c8818ba Author: grunweg <rothgami@math.hu-berlin.de> Date: Sat Jan 27 11:43:27 2024 +0000 feat(NormedSpace/Basic): add dist_smul_add_one_sub_smul_le (#9982) From sphere-eversion (slightly golfed); I'm just upstreaming it. commit ca91ff1 Author: Winston Yin <winstonyin@gmail.com> Date: Sat Jan 27 11:43:26 2024 +0000 refactor(PartialHomeomorph): make `[Nonempty s]` explicit (#9894) Subsets aren't going to have `Nonempty` instances on them, typically, so one would have to manually construct a term of `[Nonempty s]` whenever `PartialHomeomorph.subtypeRestr` is used. Turning this instance argument explicit, `(hs : Nonempty s)` would help us avoid `@PartialHomeomorph.subtypeRestr _ _ _ _` constructions or `haveI : Nonempty ...`. Its only downstream effect currently is in `ChartedSpace.lean`. commit a1bc0ac Author: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sat Jan 27 10:41:58 2024 +0000 doc(docs): fix typos (#10050) Fix minor typos in the `docs` folder. commit 15c33b6 Author: Frédéric Dupuis <dupuisf@iro.umontreal.ca> Date: Sat Jan 27 10:41:57 2024 +0000 fix: lemma given a wrong name by `to_additive` (#10049) commit 7f19636 Author: sgouezel <sebastien.gouezel@univ-rennes1.fr> Date: Sat Jan 27 10:41:57 2024 +0000 chore: factor out a lemma from the proof of Steinhaus theorem (#9907) Given a measure in a locally compact group, and a compact set `k`, then for `g` close enough to the identity, the set `g • k \ k` has arbitrarily small measure. A slightly weaker version of this fact is used implicitly in our current proof of Steinhaus theorem that `E - E` is a neighborhood of the identity if `E` has positive measure. Since I will need this lemma later on, I extract it from the proof of Steinhaus theorem in this PR. commit cb8ebaf Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Sat Jan 27 09:26:07 2024 +0000 refactor(Probability/Kernel/CondCdf): mv prod_iInter (#10037) Co-authored-by: Moritz Firsching <firsching@google.com> commit 62acece Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri Jan 26 22:26:07 2024 +0000 feat: iteratedDeriv_const_{s,}mul, iteratedDeriv_{c,}exp_const_mul (#9767) Based on @CBirkbeck's work on modular forms. commit 781af01 Author: Yury G. Kudryashov <urkud@urkud.name> Date: Fri Jan 26 20:18:23 2024 +0000 feat: drop unneeded assumptions in `IsUniform.integral_eq` (#10021) Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> commit f1802b1 Author: Eric Wieser <wieser.eric@gmail.com> Date: Fri Jan 26 19:09:11 2024 +0000 feat: Add lattice lemmas about `Sub{group,monoid}.{op,unop}` (#9860) In fact I only need the `closure` lemma, but the others are easy enough. This changes the `opEquiv`s to be order isomorphisms rather than just `Equiv`s. commit edd8f40 Author: Jireh Loreaux <loreaujy@gmail.com> Date: Fri Jan 26 18:21:29 2024 +0000 feat: link `Dilation` to `Isometry` and `Homeomorph` (#9980) commit ab48003 Author: grunweg <rothgami@math.hu-berlin.de> Date: Fri Jan 26 17:17:58 2024 +0000 chore(Calculus/ParametricIntegralInterval): small clean-ups (#10005) - collect some very common variables - use refine and \mapsto instead of refine' and => (both are preferred now) commit 1fec3c4 Author: Yury G. Kudryashov <urkud@urkud.name> Date: Fri Jan 26 13:55:43 2024 +0000 chore(Filter/Ker): move from Filter.Basic to a new file (#10023) Start moving parts of >3K lines long `Filter.Basic` to new files. commit 0085768 Author: Xavier Roblot <46200072+xroblot@users.noreply.github.com> Date: Fri Jan 26 11:59:21 2024 +0000 feat: Add `measurable_abs` (#9912) See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/measurable_abs/near/417230631) Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> commit 5821f8c Author: grunweg <rothgami@math.hu-berlin.de> Date: Fri Jan 26 11:20:53 2024 +0000 feat: add LocallyFinite.smul_{left,right} (#10020) From sphere-eversion. Will be used to show a point-wise version of `SmoothPartitionOfUnity.contMDiff_finsum_smul`. Co-authored-by: Oliver Nash <github@olivernash.org> commit e165098 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri Jan 26 11:20:52 2024 +0000 feat: add Int.le_add_one_iff (#9892) Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> commit 4529fc1 Author: Matthew Robert Ballard <matt@mrb.email> Date: Fri Jan 26 08:58:29 2024 +0000 chore(MetricSpace.PseudoMetric): make `PseudoEMetricSpace.toPseudoMetricSpaceOfDist` reducible (#10012) `PseudoEMetricSpace.toPseudoMetricSpaceOfDist` is used in instances so needs to be reducible for unification. commit f2b0b27 Author: Thomas Browning <tb65536@uw.edu> Date: Fri Jan 26 08:58:28 2024 +0000 feat(GroupTheory/GroupAction/Basic): Condition for `swap` to stabilize a set (#9945) commit a268d11 Author: grunweg <rothgami@math.hu-berlin.de> Date: Fri Jan 26 08:58:27 2024 +0000 feat: one lemma about LocallyFinite (#9813) From sphere-eversion; I'm just submitting this upstream. commit 19ab970 Author: grunweg <rothgami@math.hu-berlin.de> Date: Fri Jan 26 08:27:37 2024 +0000 feat: add PartialHomeomorph.extend_target' (#9977) Inspired by sphere-eversion; similar to `PartialEquiv.image_source_eq_target`. commit 0500719 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri Jan 26 07:29:47 2024 +0000 feat: Int.{even_sub_one,even_mul_pred_self} (#9859) Also rename `Nat.even_mul_self_pred` for consistency with `Nat.even_mul_succ_self`. commit 970a1ab Author: Oliver Nash <github@olivernash.org> Date: Fri Jan 26 04:28:56 2024 +0000 feat: the minimal polynomial is a generator of the annihilator ideal (#10008) More precisely, the goal of these changes is to make the following work: ```lean import Mathlib.FieldTheory.Minpoly.Field open Module Polynomial example {K V : Type*} [Field K] [AddCommGroup V] [Module K V] (f : End K V) : (⊤ : Submodule K[X] <| AEval K V f).annihilator = K[X] ∙ minpoly K f := by simp ``` Co-authored-by: Johan Commelin <johan@commelin.net> commit 20c7b4b Author: grunweg <rothgami@math.hu-berlin.de> Date: Fri Jan 26 03:44:15 2024 +0000 chore(Topology/Basic): re-use variables; rename a : X to x : X (#9993) Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> commit e3b6818 Author: Yury G. Kudryashov <urkud@urkud.name> Date: Fri Jan 26 03:03:09 2024 +0000 fix: `Clm` -> `CLM`, `Cle` -> `CLE` (#10018) Rename - `Complex.equivRealProdClm` → `Complex.equivRealProdCLM`; - [ ] TODO: should this one use `CLE`? - `Complex.reClm` → `Complex.reCLM`; - `Complex.imClm` → `Complex.imCLM`; - `Complex.conjLie` → `Complex.conjLIE`; - `Complex.conjCle` → `Complex.conjCLE`; - `Complex.ofRealLi` → `Complex.ofRealLI`; - `Complex.ofRealClm` → `Complex.ofRealCLM`; - `fderivInnerClm` → `fderivInnerCLM`; - `LinearPMap.adjointDomainMkClm` → `LinearPMap.adjointDomainMkCLM`; - `LinearPMap.adjointDomainMkClmExtend` → `LinearPMap.adjointDomainMkCLMExtend`; - `IsROrC.reClm` → `IsROrC.reCLM`; - `IsROrC.imClm` → `IsROrC.imCLM`; - `IsROrC.conjLie` → `IsROrC.conjLIE`; - `IsROrC.conjCle` → `IsROrC.conjCLE`; - `IsROrC.ofRealLi` → `IsROrC.ofRealLI`; - `IsROrC.ofRealClm` → `IsROrC.ofRealCLM`; - `MeasureTheory.condexpL1Clm` → `MeasureTheory.condexpL1CLM`; - `algebraMapClm` → `algebraMapCLM`; - `WeakDual.CharacterSpace.toClm` → `WeakDual.CharacterSpace.toCLM`; - `BoundedContinuousFunction.evalClm` → `BoundedContinuousFunction.evalCLM`; - `ContinuousMap.evalClm` → `ContinuousMap.evalCLM`; - `TrivSqZeroExt.fstClm` → `TrivSqZeroExt.fstClm`; - `TrivSqZeroExt.sndClm` → `TrivSqZeroExt.sndCLM`; - `TrivSqZeroExt.inlClm` → `TrivSqZeroExt.inlCLM`; - `TrivSqZeroExt.inrClm` → `TrivSqZeroExt.inrCLM` and related theorems. commit 66439f5 Author: Matthew Robert Ballard <matt@mrb.email> Date: Fri Jan 26 00:49:24 2024 +0000 chore(UniformSpace.Basic): make `UniformSpace.comap` reducible (#10010) `UniformSpace.comap` is used in instance construction so needs to be reducible for unification purposes. commit 79a9e0e Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Thu Jan 25 23:16:34 2024 +0000 refactor(Topology/Clopen): order of open and closed (#9957) Co-authored-by: Moritz Firsching <firsching@google.com> commit f9daa98 Author: grunweg <rothgami@math.hu-berlin.de> Date: Thu Jan 25 21:01:58 2024 +0000 chore(Data/ENNReal/Basic): split file (#9869) Co-authored-by: Jireh Loreaux <loreaujy@gmail.com> commit 0c4ffb6 Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Thu Jan 25 20:36:48 2024 +0000 chore(test/toAdditive): remove commented test (#9971) Co-authored-by: Moritz Firsching <firsching@google.com> commit b3052ec Author: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com> Date: Thu Jan 25 20:09:13 2024 +0000 feat: polynomial evaluation via SMul (#9139) We introduce polynomial evaluation using SMul, so polynomials can be evaluated at elements of non-associative semirings. This is most useful in the power-associative context, but power-associativity is not implemented yet. We obtain a generalization of `Polynomial.eval₂`, and in particular of the specializations `Polynomial.aeval` and `Polynomial.leval`. commit 1f2e586 Author: Alex Meiburg <alex.meiburg@gmail.com> Date: Thu Jan 25 16:42:45 2024 +0000 fix doc for LinearMap.compRight (#9997) minor typo here. An (f : M2 -> M3) induces a linear map from (M->M2) to (M->M3). Not to (M2 -> M3). Co-authored-by: Alex Meiburg <timeroot.alex@gmail.com> commit 47a9066 Author: grunweg <rothgami@math.hu-berlin.de> Date: Thu Jan 25 16:42:44 2024 +0000 feat: add `Continuous.image_connectedComponentIn_subset` (#9983) and a version for homeomorphisms. From sphere-eversion; I'm just submitting things upstream. commit e7170d3 Author: Yury G. Kudryashov <urkud@urkud.name> Date: Thu Jan 25 16:42:43 2024 +0000 feat(Topology/Basic): add TopologicalSpace.ext_isClosed (#9963) Use it to golf `PrimeSpectrum.localization_comap_inducing`. commit bd6616c Author: Yury G. Kudryashov <urkud@urkud.name> Date: Thu Jan 25 16:42:42 2024 +0000 chore(Integral/CircleTransform): golf (#9937) Motivated by @Ruben-VandeVelde's leanprover-community/mathlib#15206 commit 941d069 Author: Oliver Nash <github@olivernash.org> Date: Thu Jan 25 15:54:36 2024 +0000 feat: the torsion submodule of an irreducible element is semisimple (#9994) (provided the coefficients are a principal ideal ring) commit c27bc4e Author: Johan Commelin <johan@commelin.net> Date: Thu Jan 25 15:54:35 2024 +0000 refactor(ZMod): remove coe out of ZMod (#9839) Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Vierkantor <vierkantor@vierkantor.com> commit fe3b2b2 Author: Yury G. Kudryashov <urkud@urkud.name> Date: Thu Jan 25 14:36:36 2024 +0000 feat(Data/Sigma): add `Sigma.fst_surjective` etc (#9914) - Add `Sigma.fst_surjective`, `Sigma.fst_surjective_iff`, `Sigma.fst_injective`, and `Sigma.fst_injective_iff`. - Move `sigma_mk_injective` up. - Open `Function` namespace, drop `Function.`. - Fix indentation. commit 8853442 Author: Oliver Nash <github@olivernash.org> Date: Thu Jan 25 14:36:35 2024 +0000 feat: define semisimple linear endomorphisms (#9825) commit 0b79434 Author: Jireh Loreaux <loreaujy@gmail.com> Date: Thu Jan 25 14:02:42 2024 +0000 chore: golf `FiniteDimensional.isROrC_to_real` (#9921) commit ce79848 Author: Yury G. Kudryashov <urkud@urkud.name> Date: Thu Jan 25 13:08:16 2024 +0000 feat(Trigonometric): add lemmas about `cos x = -1 ↔ _` etc (#9878) commit 2b7478a Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Thu Jan 25 13:08:14 2024 +0000 feat: superFactorial_two_mul, superFactorial_four_mul (#7924) Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> commit c5ca57c Author: Alex J Best <alex.j.best@gmail.com> Date: Thu Jan 25 12:45:33 2024 +0000 feat: problem matchers for tests (#9552) Makes it a bit easier to see which test failed and where commit d3da7bb Author: Yuma Mizuno <mizuno.y.aj@gmail.com> Date: Thu Jan 25 12:14:10 2024 +0000 refactor(CategoryTheory/Monoidal): replace axioms with those more suitable for the whiskerings (#9991) Extracted from #6307. We replace some axioms by those more preferable when using the whiskerings instead of the tensor of morphisms. commit 2725911 Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Thu Jan 25 11:09:48 2024 +0000 chore(Algebra/Algebra/Basic): remove @s to address porting note (#9969) Co-authored-by: Moritz Firsching <firsching@google.com> commit 9a290c2 Author: grunweg <rothgami@math.hu-berlin.de> Date: Thu Jan 25 09:21:34 2024 +0000 chore(Topology/Constructions): rename most type variables (#9863) Now we use letters X and Y for topological spaces, not Greek letters. I didn't replace all letters; some lemmas need a large number of different letters. Volunteers for the last instances welcome. commit 2e59248 Author: Yuma Mizuno <mizuno.y.aj@gmail.com> Date: Thu Jan 25 06:29:39 2024 +0000 refactor(CategoryTheory/Monoidal): split the naturality condition of monoidal functors (#9988) Extracted from #6307. We replace `μ_natural` with `μ_natural_left` and `μ_natural_right` since we prefer to use the whiskerings to the tensor of morphisms in the refactor #6307. commit 8c661e5 Author: Jireh Loreaux <loreaujy@gmail.com> Date: Thu Jan 25 02:46:49 2024 +0000 feat: add `Homeomorph.subtype` for lifting homeomorphisms to subtypes (#9959) This extends `Equiv.subtypeEquiv`, which promotes `e : α ≃ β` to `e.subtypeEquiv _ : {a : α // p a} ≃ {b : β // q b}`, to homeomorphisms. We also add a missing lemma linking `Equiv.subtypeEquiv` to `Subtype.map`, and update the definition to use `Subtype.map` also. commit 0c34368 Author: grunweg <rothgami@math.hu-berlin.de> Date: Thu Jan 25 01:23:40 2024 +0000 feat: sigma-compact measure zero sets are meagre (#7640) Co-authored-by: Mario Carneiro <di.gama@gmail.com> commit ad22323 Author: Eric Wieser <wieser.eric@gmail.com> Date: Thu Jan 25 00:17:40 2024 +0000 feat: two lemmas about division (#9966) commit e88d290 Author: Oliver Nash <github@olivernash.org> Date: Wed Jan 24 22:51:33 2024 +0000 chore: remove porting note after `simp` fix (#9974) commit a686ba8 Author: grunweg <rothgami@math.hu-berlin.de> Date: Wed Jan 24 20:52:37 2024 +0000 feat: finite products/sums of differentiable maps into smooth commutative monoids are differentiable (#9775) From sphere-eversion; I'm just upstreaming this. Co-authored-by: Oliver Nash <github@olivernash.org> commit 0aa016e Author: Matthew Robert Ballard <matt@mrb.email> Date: Wed Jan 24 18:17:19 2024 +0000 chore(Algebra.Basic): override `toFun` and `smul` in `Algebra.id` (#9949) The current definition of `Algebra.id` is `(RingHom.id _).toAlgebra`. The problem with this is that `RingHom.id` is a `def` and is not reducible. Thus Lean will often refuse to unfold it causing unification to fail unecessarily in typeclass searches. This overrides the data fields from `RingHom.id`. commit 725f123 Author: Anne Baanen <vierkantor@vierkantor.com> Date: Wed Jan 24 15:59:29 2024 +0000 perf: de-prioritize `Subalgebra.algebra'` and `IntermediateField.algebra'` (#9936) Like in #9655, these instances tend to be slow to fail, so we should assign them a low priority. Zulip discussions: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Algebra.2Eid.20for.20IntermediateField https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Timeout.20in.20Submodule.20.28.F0.9D.93.9E.20K.29.20.28.F0.9D.93.9E.20K.29 Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> commit 4fe0086 Author: Yury G. Kudryashov <urkud@urkud.name> Date: Wed Jan 24 15:59:27 2024 +0000 feat(UpperHalfPlane): add positivity extensions (#9545) commit 9a8dc7a Author: Christian Merten <christian@merten.dev> Date: Wed Jan 24 14:31:55 2024 +0000 feat(CategoryTheory/Galois): finite `G`-sets are a `PreGaloisCategory` (#9879) We show that the category of finite `G`-sets is a `PreGaloisCategory` and the forgetful functor to finite sets is a `FibreFunctor`. commit d1054e1 Author: grunweg <rothgami@math.hu-berlin.de> Date: Wed Jan 24 14:31:54 2024 +0000 chore(Topology): remove autoImplicit from most remaining files (#9865) commit 00202e4 Author: grunweg <rothgami@math.hu-berlin.de> Date: Wed Jan 24 14:31:52 2024 +0000 feat(Topology/Support): add tsupport_smul_{left,right} (#9778) - rename `Function.support_smul_subset_right` to `Function.support_const_smul_subset` From sphere-eversion; I'm just upstreaming it. Co-authored-by: grunweg <grunweg@posteo.de> commit fac72bc Author: Scott Morrison <scott@tqft.net> Date: Wed Jan 24 13:11:22 2024 +0000 chore: bump dependencies (#9962) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> commit 02240d5 Author: Eric Wieser <wieser.eric@gmail.com> Date: Wed Jan 24 13:11:21 2024 +0000 refactor: move `Archimedean` instances to `Order/Archimedean` (#9950) We already have the instances for `ℕ`, `ℤ`, and `ℚ` in this file, so adding `NNRat` doesn't feel that out of place, as it completes this {negation,division} lattice. Follows on from #9917. These changes knock off 132 dependencies from `NNRat`, though adds more to `Archimedean`. I think this is acceptable; we need `NNRat` to be super early if we want to be able to use it in norm_num, and the depth of `Archimedean` will reduce with `NNRat` as I work towards this. commit e61934e Author: damiano <adomani@gmail.com> Date: Wed Jan 24 13:11:20 2024 +0000 Add `Lattice ℤ` instance for computability (#9946) The file `Data.Int.ConditionallyCompleteOrder` defines a noncomputable instance of `ConditionallyCompleteLinearOrder` on `ℤ`. This noncomputable instance is picked up by the typeclass search when looking for a `Lattice` instance on `ℤ`, making, for instance, `abs` noncomputable on `ℤ`. This PR restores the computability of `Lattice ℤ`. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/No.20more.20.60Abs.60.3F/near/417546479) commit 6694f75 Author: Yury G. Kudryashov <urkud@urkud.name> Date: Wed Jan 24 10:41:24 2024 +0000 chore(Topology/Basic): rename variables (#9956) Use `X`, `Y`, `Z` for topological spaces. commit 46e6944 Author: Winston Yin <winstonyin@gmail.com> Date: Wed Jan 24 10:06:42 2024 +0000 chore: rename `StructureGroupoid.eq_on_source'` to `StructureGroupoid.mem_of_eqOnSource'` (#9802) Since it refers to `PartialEquiv.EqOnSource`, the correct naming scheme should not be snake case `eq_on_source`. I also added `mem_of_` because that's the target of the lemma, while `EqOnSource` is just a hypothesis. There are no added lemmas or docstrings in this PR. It's all just renaming. commit cf5ad94 Author: Scott Morrison <scott@tqft.net> Date: Wed Jan 24 03:45:17 2024 +0000 chore: bump Std and Aesop (#9948) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> commit 0faddd8 Author: Yaël Dillies <yael.dillies@gmail.com> Date: Wed Jan 24 02:51:10 2024 +0000 feat: `n • v` and `v` are on the same ray (#9104) From LeanAPAP commit 6219c28 Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Date: Wed Jan 24 02:24:12 2024 +0000 feat: transfer of graph properties over maps (#9708) Part of #9317.
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.
In preparation for Jordan-Chevalley-Dunford
I can break this PR into smaller pieces on request.