Changelog
2025-04-18 00:22 5cffd162
feat: generalize `TwoSidedIdeal.matricesOver` to `RingCon` (#23641) …
5 files19 theorems5 defs
2025-04-17 23:56 dad08fa3
feat: `PiFin.mkLiteralQ` and `Matrix.mkLiteralQ` (#24101) …
4 files2 defs
2025-04-17 22:12 35533054
feat(BigOperators/Ring): add `Finset.prod_neg` (#24146)
1 files1 theorems
2025-04-17 18:29 579c35b7
feat(Combinatorics/SimpleGraph): miscellaneous walk lemmas (#22242) …
5 files8 theorems
2025-04-17 16:41 9ec5b5d8
feat: Nat.toDigits_length (#24126) …
1 files3 theorems
2025-04-17 15:55 4a76948a
fix(ByContra hover): hover over by_contra! gets its doc-string back (#24087) …
1 files
2025-04-17 14:45 446b459f
chore: replace mono by gcongr (#23968) …
1 files
2025-04-17 13:52 1f4ab9d5
feat: add lemma `Submodule.length_lt` (#24133) …
3 files4 theorems
2025-04-17 13:24 9ebc6664
feat(Interval/Finset/Fin): add lemmas about `Finset.image` (#23420) …
4 files154 theorems
2025-04-17 11:01 6fb295ce
feat: `x.swap < (b, a) ↔ x < (a, b)` (#24124)
1 files7 theorems
2025-04-17 08:00 d4fc0372
chore: deprecate the file `AnalyticManifold` (#20979) …
3 files10 theorems4 defs
2025-04-17 01:59 5d914f06
feat: add a `ToExpr` instance for `Multiset` (#24014) …
2 files
2025-04-17 01:13 e3601d1f
chore: automatically additivize IsScalarTower (#24115)
12 files1 theorems
2025-04-17 00:27 5fcae8b6
feat: additivise `Irreducible` (#22904) …
7 files34 theorems3 structures
2025-04-16 22:42 3821c1d2
chore(Topology.Algebra.Valued.WithVal): clean up typeclass assumptions (#24125) …
1 files1 defs
2025-04-16 20:00 422961d2
chore: cleanup API around order of univariate power series (#24072) …
4 files27 theorems2 defs
2025-04-16 15:35 583dd351
feat (RingTheory/PowerSeries/Order) : compute order of power and generalize (#23993) …
3 files14 theorems
2025-04-16 13:50 da9d909e
chore: remove TODO from docstring (#24111) …
1 files
2025-04-16 12:10 143cf10c
fix: homeomorphisms->homomorphisms (#24097)
1 files
2025-04-16 11:45 df25981b
fix(nolints.yml): continue gracefully if no changes were found (#24110) …
1 files
2025-04-16 09:34 79e9db7b
feat(Lean/ToExpr): add helper functions to create `Expr` for finsets/sets/multisets (#23025) …
3 files1 defs
2025-04-16 09:34 9c97e7a8
feat(NumberField/CanonicalEmbedding/NormLeOne): compute the volume of `NormLeOne` (#22777) …
6 files20 theorems
2025-04-16 08:54 1a64c90d
feat(NumberField/Discriminant): better lower bound for totally complex number fields (#24076)
2 files7 theorems
2025-04-15 18:40 2f52b383
chore(RingTheory): fix variable in FilteredAlgebra.Basic (#24071) …
1 files
2025-04-15 17:56 53b9fb34
chore(Fin): fix some `@[simp]` lemmas (#23967) …
3 files5 theorems
2025-04-15 16:58 595daf8e
feat: definition + basic results for chains / strings in root pairings (#24077)
8 files28 theorems4 defs
2025-04-15 16:43 ce5e0f61
fix(nolints.yml): move `print Lean version` step after the installation of Lean (#24088) …
1 files
2025-04-15 16:43 fad8b5dc
feat(CategoryTheory/Limits): preservation of multicoequalizers (#22205)
3 files5 defs
2025-04-15 16:43 b533ec6d
feat(CategoryTheory/Limits): multicoequalizers attached to linear orders (#22203) …
1 files1 theorems7 defs1 structures
2025-04-15 16:20 bc0f16d2
chore(Archimedean/Basic): minor cleanup (#23854)
1 files2 theorems
2025-04-15 15:31 fb24ff15
chore(CategoryTheory/Over): fix name of `Under.pullbackComp` (#24084)
1 files2 defs
2025-04-15 15:08 f6d7b217
doc: correct scope name (#24085)
1 files
2025-04-15 14:18 cd81a4df
chore: exchange `Nat.sub_lt_iff_lt_add` and `Nat.sub_lt_iff_lt_add'` (#24080) …
4 files
2025-04-15 13:58 14e33038
feat(CategoryTheory): `ChosenFiniteProducts (Over X)` (#21399) …
2 files30 theorems1 defs
2025-04-15 12:42 bbccb92b
chore(BumpFunction/Convolution): drop an assumption (#24063) …
1 files2 theorems
2025-04-15 12:02 091be7a8
feat(LpSeminorm/Basic): generalise monotonicity section to enorm (#23707) …
4 files9 theorems
2025-04-15 10:53 07e34201
feat (Yoneda): (co)representing objects are unique up to iso (#24059) …
1 files3 defs
2025-04-15 10:53 aa17f77c
chore(Finsupp/Interval): remove `open scoped Classical` (#24055) …
4 files
2025-04-15 10:53 a9eda3d7
feat: add characterisation of closed interval for locally-finite conditionally complete linear orders (#23910)
3 files7 theorems
2025-04-15 10:46 bec84036
chore: split `MeasureTheory.Integral.SetToL1` (#24075) …
3 files94 theorems6 defs
2025-04-15 09:57 69393803
feat: a binary fan in `Over X` is the same thing as a pullback cone to `X` (#23723) …
2 files24 theorems20 defs
2025-04-15 09:16 96081764
feat(RingTheory/LocalRing): results for non-local rings (#24043)
2 files5 theorems
2025-04-15 08:42 6b8c3cca
chore: split `MeasureTheory.Integral.SetIntegral` (#24070) …
28 files310 theorems1 defs
2025-04-15 08:18 679ed8e6
chore: move and rename `eval_of_algHom` (#23952) …
2 files2 theorems
2025-04-15 07:29 d730d225
chore(Analysis/Convex/Combination): remove `open scoped Classical` from theorems (#24057) …
1 files5 theorems
2025-04-15 07:29 dabe44e6
chore(*): rename more type vars for *rings (#24022)
3 files17 theorems8 defs1 structures
2025-04-15 07:29 f1c60d39
feat(Set): restricting the identity function (#23995)
1 files1 theorems
2025-04-15 07:00 e7b8f4e1
feat(Topology): closure of subsingleton is self (#24062) …
1 files2 theorems
2025-04-15 07:00 f4ae6b85
chore: golf copy of Pi.single (#24061)
1 files
2025-04-15 07:00 fa14299f
feat(Algebra/Algebra/Subalgebra): `Algebra.adjoin_singleton_le` (#24048) …
1 files1 theorems