Changelog

2024-10-04 23:30 11fa9c00
chore(Analysis/InnerProductSpace/Dual): weaken assumptions to SeminormedAddCommGroup (#17416) …
1 files
2024-10-04 21:26 584dd88a
feat(CategoryTheory/Limits): generalize universes for preserving finite products (#17408)
2 files
2024-10-04 21:26 d2499a7b
feat (Mathlib/SetTheory/Ordinal/Arithmetic): add bounded recursion on ordinals (#16663) …
1 files3 theorems1 defs
2024-10-04 20:24 2f7bdced
feat: not_odd_zero for Nat and Int (#17419) …
3 files2 theorems
2024-10-04 20:24 25571772
chore: update Mathlib dependencies 2024-10-04 (#17414) …
1 files
2024-10-04 20:24 a0785003
feat(AlgebraicGeometry): add `resLE` (#17264) …
4 files14 theorems1 defs
2024-10-04 20:24 4e011876
chore(RingTheory/Valuation): change implicitness in `Valuation.IsEquiv` lemmas (#17051) …
2 files
2024-10-04 20:24 811c9e37
feat(AlgebraicGeometry/EllipticCurve/NormalForms): some normal forms of elliptic curves (#16864) …
3 files116 theorems7 defs
2024-10-04 20:24 c3020c3e
chore(NumberTheory/LucasPrimality): golf theorem (#16848)
1 files
2024-10-04 20:24 dcfb7823
feat: Adding/removing an element from a product of finsets (#7898) …
1 files14 theorems
2024-10-04 18:34 dfcf58dd
chore: make `Integrable.of_finite` have no explicit argument (#17323) …
3 files2 theorems
2024-10-04 17:27 38cbcf05
feat(Algebra/Group/Equiv): add two simp lemmas for `MulEquivClass` (#17085) …
1 files2 theorems
2024-10-04 14:05 5e050d47
chore(*): assume `Subsingleton Mˣ` instead of `Unique Mˣ` (#17391) …
9 files8 theorems
2024-10-04 14:05 616c3bfe
chore(Analytic/CPolynomial): move&generalize some lemmas (#17390) …
2 files9 theorems
2024-10-04 14:05 5269859b
chore(Galois/Basic): `Fintype` → `Finite` (#17382)
1 files
2024-10-04 14:05 411a67a2
chore: generalise even more lemmas from `LinearOrderedField` to `GroupWithZero` (#17378)
30 files22 theorems
2024-10-04 14:05 4e27a8d9
ci(update_dependencies_zulip): Add actionable message when lake update fails (#17331)
1 files
2024-10-04 14:05 ca6941cb
chore: `Set.divisionCommMonoid` scoped earlier (#17301) …
2 files
2024-10-04 14:05 2ae9a800
feat: `a = cast e b ↔ HEq a b` (#17294) …
1 files2 theorems
2024-10-04 14:05 674ce265
feat(Data/Multiset/Basic): add lemma on `Multiset` (#17273) …
1 files1 theorems
2024-10-04 14:05 8033cba2
feat(NumberTheory/RamificationInertia): ramification index and inertia degree in tower of algebras (#17160) …
4 files8 theorems
2024-10-04 14:05 eeedb316
chore(Data/Set): split Data/Set/Function (#17091) …
5 files44 theorems
2024-10-04 14:05 6039b328
feat(Data/Int/WithZero): add WithZeroMultIntToNNReal (#15741) …
2 files5 theorems1 defs
2024-10-04 11:14 5ddd0ae2
feat(CategoryTheory): lemmas about `descOfIsLeftKanExtension` for pointwise left Kan extensions (+dual) (#17383)
1 files2 theorems2 defs
2024-10-04 11:14 44f94cd9
chore(CompHausLike): add constant morphisms (#17381)
1 files1 theorems1 defs
2024-10-04 11:14 10237afb
feat (Analysis/Normed/Group): ultrametric normed groups are nonarchimedean (#17262) …
3 files2 defs
2024-10-04 11:14 fafd1f69
chore: Delete declarations deprecated in 2023 (#17193) …
24 files7 theorems
2024-10-04 11:14 7b3092eb
feat(Condensed): discrete condensed modules are given by locally constant maps (#15569) …
2 files2 defs
2024-10-04 10:12 47ada502
feat: the canonical bilinear form of the root system of a Lie algebra is the Killing form (#17392) …
5 files3 theorems
2024-10-04 10:12 2a16a7b0
refactor(CategoryTheory): generalize universes for representable functors (#17389) …
5 files19 theorems6 defs2 structures
2024-10-04 10:12 2dcb3ba7
chore(Profinite): add Fintype instances (#17380)
2 files
2024-10-04 10:12 12bdcfbb
feat(RingTheory): target local closure of property of ring homomorphisms (#17032) …
3 files8 theorems1 defs
2024-10-04 10:12 6d453919
feat(Data/Finset): right elements of a finset in the sum type (#17014)
2 files36 theorems2 defs
2024-10-04 10:12 8834646c
feat(Topology/Group): Open normal subgroup (#16980) …
1 files1 theorems2 structures
2024-10-04 10:12 58523222
feat(Tactic/Algebraize): add algebraize tactic (#16217) …
10 files7 defs1 structures
2024-10-04 09:10 b758def5
chore: bump toolchain to v4.13.0-rc3 (#17401)
1 files
2024-10-04 08:21 4e8b403f
feat: the cosine of `π / 5` is `(1 + √5) / 4` (#17393)
4 files8 theorems
2024-10-04 08:03 96f08e76
chore: update Mathlib dependencies 2024-10-04 (#17397) …
1 files
2024-10-04 07:26 3ad544d9
ci(nightly_detect_failure): add actionable message in case of failure (#17329) …
1 files
2024-10-04 06:17 b0bcf46f
feat: if a function is analytic on a set, its derivative also is, even if the space is not complete (#17221) …
3 files32 theorems1 defs
2024-10-04 04:46 630c6324
refactor(Algebra/Field/Subfield): minor golfing (#17376)
1 files
2024-10-04 04:46 a083bae2
feat(RingTheory): define two-sided Jacobson radical (#17341) …
4 files10 theorems2 defs
2024-10-04 04:46 149d450d
feat: Order properties of `Pi.single` (#17281) …
1 files3 theorems
2024-10-04 04:46 6dd0053d
feat: Big operators indexed by an interval (#17280) …
2 files12 theorems
2024-10-04 04:46 7e655050
feat: Order instances for `MulOpposite`/`AddOpposite` (#17201) …
3 files14 theorems
2024-10-04 04:46 99b8e711
feat(Data/*/Sort): lemmas on sorted lists (#16078) …
4 files8 theorems
2024-10-04 03:58 435c3d7b
chore(Finset): remove old-style spellings (#17327) …
3 files4 theorems
2024-10-04 03:33 1c37f1e9
chore: bump toolchain to v4.13.0-rc2 (#17377) …
232 files55 theorems
2024-10-03 20:47 3ca1060d
chore: Rename `UniformEmbedding` to `IsUniformEmbedding` (#17295) …
48 files115 theorems2 structures
2024-10-03 20:47 aeefd817
refactor: Let `positivity` handle `ENNReal`-valued `ofNat` (#17212) …
2 files1 theorems