Changelog
2024-12-02 01:32 dde4f2ec
feat: an equality condition for AM-GM inequality (#19435) …
1 files3 theorems
2024-12-02 01:23 7c5e3712
chore: update Mathlib dependencies 2024-12-02 (#19672) …
0 files
2024-12-02 01:14 4bbdccd9
chore: bump toolchain to v4.14.0 (#19673)
3 files
2024-12-01 22:43 8639aea3
feat: `Polynomial.map f` strictly decreases the degree if `f p.leadingCoeff = 0` (#19411) …
13 files5 theorems
2024-12-01 21:58 439bd582
ci(dependabot.yml): use glob syntax in config... (#19662) …
1 files
2024-12-01 19:53 6926cee9
fix(FieldTheory/AlgebraicClosure): `algebraicClosure.AlgEquiv.algebraicClosure` -> `AlgEquiv.algebraicClosure` (#19642)
1 files
2024-12-01 16:15 2aefce62
chore: move `Topology.Support` to `Topology.Algebra.Support` (#19651) …
8 files
2024-12-01 14:12 65cc5434
chore: add location of build.in.yml to directories checked by dependabot (#18712) …
1 files
2024-12-01 13:50 9d16cdd2
chore: update benchmark runner for leanprover/lean4#5684 (#19656) …
1 files
2024-12-01 11:18 a3fcd535
chore(Algebra/Data/Order/Floor): remove todo on `fract_div_intCast_eq… (#19652) …
1 files
2024-12-01 10:47 90f9e991
chore: remove PartENat from PowerSeries (#19622)
5 files21 theorems2 defs
2024-12-01 09:59 e4876c14
chore: delete deprecated lemmas (#19627) …
9 files
2024-12-01 09:59 822e8564
feat(NumberTheory): Abel summation (#19289) …
4 files5 theorems
2024-12-01 09:59 c8203667
feat(Algebra/MvPolynomial/Degrees): degreeOf_mul_X_eq_degreeOf_add_one_iff (#17553)
2 files2 theorems
2024-12-01 09:31 81b5c5ca
feat(FieldTheory/Galois): Lemmas of galois theory (#16979) …
4 files7 theorems1 defs
2024-12-01 08:03 b8b8a288
chore: update benchmark runner for leanprover/lean4#5684 (#19649) …
1 files
2024-12-01 01:39 a1f01bd5
refactor(Algebra/Bilinear): generalize to non-commutative base rings (#19232) …
2 files12 theorems4 defs
2024-12-01 00:37 c769c4fb
chore(scripts): update nolints.json (#19647) …
1 files
2024-12-01 00:08 fa4bdc15
feat: introduce ENat.card, and use it in place of PartENat.card (#19624)
6 files25 theorems1 defs
2024-11-30 21:42 6c4358ea
chore: don't import conformal maps in Behrend's construction (#19638)
11 files4 theorems
2024-11-30 19:56 4fafb9f5
feat(CategoryTheory): Relation between the Grothendieck construction and `AsSmall` (#19539)
4 files2 theorems5 defs
2024-11-30 18:25 883af569
chore: remove `normalizeScaleRoots` (#6183) …
8 files25 theorems
2024-11-30 09:42 ba7312b5
chore: move definition of ENat and PNat out of Order.TypeTags (#19485) …
7 files4 theorems8 defs
2024-11-30 09:21 ad2e8f11
chore(RingTheory): split up `Algebraic.lean` (#19370) …
21 files51 theorems8 defs
2024-11-30 09:05 c73ab4cd
feat(CategoryTheory/SmallObject/Iteration): existence of objects (bot and succ cases) (#19047)
3 files7 theorems9 defs
2024-11-30 01:55 eb9d9b39
chore: fix names `{un}op_non{neg,pos}` (#19575)
1 files4 theorems
2024-11-30 00:03 21608d1f
feat(Algebra/Homology/Embedding): dualise extend (#19560) …
1 files2 theorems
2024-11-30 00:03 e1064d2a
feat(Algebra/Homology): more duality results (#19559) …
4 files19 theorems5 defs
2024-11-30 00:03 8a86c2c4
feat(Algebra/Homology/Embedding): the canonical truncation functor `trunGEFunctor` (#19543) …
1 files6 theorems
2024-11-30 00:03 6ce78a15
feat(Algebra/Polynomial/Roots): for a monic polynomial `p`, `p.roots.map f = (p.map f).roots` if `p.roots.card = p.natDegree` (#19430) …
1 files2 theorems
2024-11-30 00:03 3d4e9f41
chore: change associativity of `+ᵥ` from `infixl` to `infixr` (#19321) …
7 files10 theorems
2024-11-30 00:03 f33352ab
feat(LinearAlgebra/Matrix/Permanent): smul (#19307) …
1 files3 theorems
2024-11-30 00:02 9bdc1af7
feat(Algebra/Homology/Embedding): the left homology of an extension of homological complexes (#18502) …
3 files3 theorems4 defs
2024-11-29 23:24 c6be01e3
chore: split out map_dvd (#19565)
7 files6 theorems
2024-11-29 22:48 cee87aa2
refactor(AlgebraicGeometry/EllipticCurve/*): add `WeierstrassCurve.IsElliptic` and remove `EllipticCurve` (#18531) …
8 files112 theorems16 defs1 structures
2024-11-29 21:45 67afcb68
feat: update the `ContDiff` definition to integrate analytic functions in the hierarchy (#17152) …
30 files104 theorems1 defs
2024-11-29 19:27 f9e900aa
chore(Filter/Prod): drop `Filter.prod`, use `SProd` instead (#18315) …
12 files17 theorems
2024-11-29 15:48 cf80f345
chore: update Mathlib dependencies 2024-11-29 (#19608) …
1 files
2024-11-29 14:47 08ada333
chore: update Mathlib dependencies 2024-11-29 (#19605) …
1 files
2024-11-29 12:22 49652777
feat(AlgebraicGeometry): the small site associated to a morphism property (#18945) …
4 files12 theorems4 defs
2024-11-29 11:09 90f062fe
feat(NumberTheory/EllipticDivisibilitySequence): extend even-odd recursion to integers (#13786) …
5 files26 theorems
2024-11-29 10:59 9c9b448e
feat: Label zulip PR links with awaiting-author emoji (#19599) …
2 files
2024-11-29 09:51 8f06fcac
feat(Combinatorics/SimpleGraph/Matching): add `IsCycles` and `IsAlternating` with basic results (#19250) …
1 files3 theorems2 defs
2024-11-29 08:51 1426b9e5
chore: update Mathlib dependencies 2024-11-29 (#19598) …
1 files
2024-11-29 06:22 ab780650
fix: add `realm_emoji` (and `emoji_code`) to auto-zulip reactions (#19597) …
1 files
2024-11-29 05:06 2e513bec
chore: update Mathlib dependencies 2024-11-29 (#19595) …
1 files
2024-11-29 04:10 a3890372
feat(Order/InitialSeg): initial segments preserve successor limits (#19053) …
4 files17 theorems
2024-11-29 04:10 8e5beeaf
refactor(Order/WellFounded): deprecate `WellFounded.succ` (#18238) …
1 files
2024-11-29 03:48 27d7119d
chore(SetTheory/Ordinal/Basic): deprecate results on `WellOrder` (#18208) …
1 files3 theorems
2024-11-29 03:02 dade1b8d
chore: bump toolchain to v4.14.0-rc3 (#19594) …
1 files