Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
commit 4fcf5bd Author: Scott Morrison <[email protected]> Date: Tue Jan 30 04:00:55 2024 +0000 chore: bump Std to leanprover-community/batteries#566 (#10117) Co-authored-by: Scott Morrison <[email protected]> commit 99afa84 Author: Yury G. Kudryashov <[email protected]> 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 <[email protected]> Date: Tue Jan 30 02:26:16 2024 +0000 fix: use getTransparency in librarySearch SolveByElim.Config (#10052) commit 9cc09f6 Author: Yury G. Kudryashov <[email protected]> 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 <[email protected]> Date: Tue Jan 30 02:26:14 2024 +0000 feat: characterize "eventually" in a subtype (#7568) Co-authored-by: Anatole Dedecker <[email protected]> Co-authored-by: ADedecker <[email protected]> commit d3a6c9f Author: Scott Morrison <[email protected]> Date: Tue Jan 30 01:07:06 2024 +0000 chore: bump Std to leanprover-community/batteries#242 (#10104) Co-authored-by: Scott Morrison <[email protected]> commit 132e511 Author: Winston Yin <[email protected]> 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 <[email protected]> Co-authored-by: Michael Rothgang <[email protected]> commit b4d01dc Author: Moritz Firsching <[email protected]> Date: Mon Jan 29 21:32:09 2024 +0000 refactor(MeasureTheory/Function/L1Space): rm two porting notes (#10056) Co-authored-by: Moritz Firsching <[email protected]> commit 7458f0e Author: Yury G. Kudryashov <[email protected]> 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 <[email protected]> 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 <[email protected]> Date: Mon Jan 29 16:54:51 2024 +0000 chore(Data/List/Rotate): add `@[simp]` to `rotate_replicate` (#10106) commit 89f9777 Author: Scott Morrison <[email protected]> Date: Mon Jan 29 15:34:18 2024 +0000 chore: fix Punit->PUnit in CommMon_ (#10089) Co-authored-by: Scott Morrison <[email protected]> commit 00b71ef Author: Moritz Firsching <[email protected]> Date: Mon Jan 29 14:47:04 2024 +0000 refactor(Probability/Kernel/CondCdf): mv tendsto_of_antitone (#10046) Co-authored-by: Moritz Firsching <[email protected]> commit 68c771a Author: Pietro Monticone <[email protected]> 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 <[email protected]> Date: Mon Jan 29 13:15:22 2024 +0000 chore(Analysis/SpecialFunctions/JapaneseBracket): restore measurability (#10054) Co-authored-by: Moritz Firsching <[email protected]> commit cea4f7a Author: Scott Morrison <[email protected]> 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 <[email protected]> commit 197378a Author: Adam Topaz <[email protected]> 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 <[email protected]> Date: Mon Jan 29 07:53:36 2024 +0000 chore(Order/Filter/ListTraverse): move from `Basic` (#10048) commit a4c1d9d Author: sgouezel <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> commit f5a69ea Author: Kevin Buzzard <[email protected]> Date: Mon Jan 29 01:14:44 2024 +0000 docs(Algebra/Algebra/Basic): get the type right (#10055) commit 995b1af Author: Pietro Monticone <[email protected]> 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 <[email protected]> Date: Sun Jan 28 23:24:42 2024 +0000 feat(Convex/Gauge): add `continuousAt_gauge` (#9911) commit 9f35a08 Author: Oliver Nash <[email protected]> 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 <[email protected]> commit e975e78 Author: Yury G. Kudryashov <[email protected]> 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 <[email protected]> Date: Sun Jan 28 09:50:58 2024 +0000 refactor(Probability/Kernel/CondCdf): mv some theorems (#10036) Co-authored-by: Moritz Firsching <[email protected]> commit e8bfb67 Author: Moritz Firsching <[email protected]> Date: Sun Jan 28 09:07:45 2024 +0000 refactor(Probability/Kernel/CondCdf): mv ofReal_cinfi (#10044) Co-authored-by: Moritz Firsching <[email protected]> commit d5277c9 Author: Matthew Robert Ballard <[email protected]> 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 <[email protected]> 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 <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> commit e4e10f9 Author: Michael Stoll <[email protected]> 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 <[email protected]> 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 <[email protected]> commit f1919fd Author: Yuma Mizuno <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> Date: Sat Jan 27 10:41:57 2024 +0000 fix: lemma given a wrong name by `to_additive` (#10049) commit 7f19636 Author: sgouezel <[email protected]> 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 <[email protected]> Date: Sat Jan 27 09:26:07 2024 +0000 refactor(Probability/Kernel/CondCdf): mv prod_iInter (#10037) Co-authored-by: Moritz Firsching <[email protected]> commit 62acece Author: Ruben Van de Velde <[email protected]> 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 <[email protected]> Date: Fri Jan 26 20:18:23 2024 +0000 feat: drop unneeded assumptions in `IsUniform.integral_eq` (#10021) Co-authored-by: sgouezel <[email protected]> commit f1802b1 Author: Eric Wieser <[email protected]> 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 <[email protected]> Date: Fri Jan 26 18:21:29 2024 +0000 feat: link `Dilation` to `Isometry` and `Homeomorph` (#9980) commit ab48003 Author: grunweg <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> commit 5821f8c Author: grunweg <[email protected]> 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 <[email protected]> commit e165098 Author: Ruben Van de Velde <[email protected]> Date: Fri Jan 26 11:20:52 2024 +0000 feat: add Int.le_add_one_iff (#9892) Co-authored-by: Yury G. Kudryashov <[email protected]> commit 4529fc1 Author: Matthew Robert Ballard <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> commit 20c7b4b Author: grunweg <[email protected]> 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 <[email protected]> Co-authored-by: Yury G. Kudryashov <[email protected]> commit e3b6818 Author: Yury G. Kudryashov <[email protected]> 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 <[email protected]> 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 <[email protected]> Date: Thu Jan 25 23:16:34 2024 +0000 refactor(Topology/Clopen): order of open and closed (#9957) Co-authored-by: Moritz Firsching <[email protected]> commit f9daa98 Author: grunweg <[email protected]> Date: Thu Jan 25 21:01:58 2024 +0000 chore(Data/ENNReal/Basic): split file (#9869) Co-authored-by: Jireh Loreaux <[email protected]> commit 0c4ffb6 Author: Moritz Firsching <[email protected]> Date: Thu Jan 25 20:36:48 2024 +0000 chore(test/toAdditive): remove commented test (#9971) Co-authored-by: Moritz Firsching <[email protected]> commit b3052ec Author: Scott Carnahan <[email protected]> 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 <[email protected]> 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 <[email protected]> commit 47a9066 Author: grunweg <[email protected]> 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 <[email protected]> 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 <[email protected]> Date: Thu Jan 25 16:42:42 2024 +0000 chore(Integral/CircleTransform): golf (#9937) Motivated by @Ruben-VandeVelde's leanprover-community/mathlib3#15206 commit 941d069 Author: Oliver Nash <[email protected]> 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 <[email protected]> Date: Thu Jan 25 15:54:35 2024 +0000 refactor(ZMod): remove coe out of ZMod (#9839) Co-authored-by: Ruben Van de Velde <[email protected]> Co-authored-by: Vierkantor <[email protected]> commit fe3b2b2 Author: Yury G. Kudryashov <[email protected]> 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 <[email protected]> Date: Thu Jan 25 14:36:35 2024 +0000 feat: define semisimple linear endomorphisms (#9825) commit 0b79434 Author: Jireh Loreaux <[email protected]> Date: Thu Jan 25 14:02:42 2024 +0000 chore: golf `FiniteDimensional.isROrC_to_real` (#9921) commit ce79848 Author: Yury G. Kudryashov <[email protected]> Date: Thu Jan 25 13:08:16 2024 +0000 feat(Trigonometric): add lemmas about `cos x = -1 ↔ _` etc (#9878) commit 2b7478a Author: Moritz Firsching <[email protected]> Date: Thu Jan 25 13:08:14 2024 +0000 feat: superFactorial_two_mul, superFactorial_four_mul (#7924) Co-authored-by: Moritz Firsching <[email protected]> Co-authored-by: Yury G. Kudryashov <[email protected]> commit c5ca57c Author: Alex J Best <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> commit 9a290c2 Author: grunweg <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> Date: Thu Jan 25 01:23:40 2024 +0000 feat: sigma-compact measure zero sets are meagre (#7640) Co-authored-by: Mario Carneiro <[email protected]> commit ad22323 Author: Eric Wieser <[email protected]> Date: Thu Jan 25 00:17:40 2024 +0000 feat: two lemmas about division (#9966) commit e88d290 Author: Oliver Nash <[email protected]> Date: Wed Jan 24 22:51:33 2024 +0000 chore: remove porting note after `simp` fix (#9974) commit a686ba8 Author: grunweg <[email protected]> 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 <[email protected]> commit 0aa016e Author: Matthew Robert Ballard <[email protected]> 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 <[email protected]> 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 <[email protected]> commit 4fe0086 Author: Yury G. Kudryashov <[email protected]> Date: Wed Jan 24 15:59:27 2024 +0000 feat(UpperHalfPlane): add positivity extensions (#9545) commit 9a8dc7a Author: Christian Merten <[email protected]> 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 <[email protected]> Date: Wed Jan 24 14:31:54 2024 +0000 chore(Topology): remove autoImplicit from most remaining files (#9865) commit 00202e4 Author: grunweg <[email protected]> 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 <[email protected]> commit fac72bc Author: Scott Morrison <[email protected]> Date: Wed Jan 24 13:11:22 2024 +0000 chore: bump dependencies (#9962) Co-authored-by: Scott Morrison <[email protected]> commit 02240d5 Author: Eric Wieser <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> Date: Wed Jan 24 03:45:17 2024 +0000 chore: bump Std and Aesop (#9948) Co-authored-by: Scott Morrison <[email protected]> commit 0faddd8 Author: Yaël Dillies <[email protected]> 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 <[email protected]> Date: Wed Jan 24 02:24:12 2024 +0000 feat: transfer of graph properties over maps (#9708) Part of #9317.
- Loading branch information
1 parent
a95b91b
commit c03f829