Changelog
2025-06-24 02:26 a119fcbe
feat: small API lemma about ContinuousMap[Zero].mkD (#26250)
2 files2 theorems
2025-06-24 02:04 20584e89
feat: `norm_num` plugin for `Nat.clog` (#26317)
2 files1 theorems2 defs
2025-06-23 21:11 108ee02a
fix(maintainer_merge_wf_run.yml): add missing AUTHOR env var (#26324) …
1 files
2025-06-23 20:37 f2e9b91e
fix(maintainer_*_wf_run.yml): correct syntax for multiline strings (#26323) …
2 files
2025-06-23 20:05 8eb1f2fe
chore: rewrite maintainer_*.yml to work from forks (#26288) …
4 files
2025-06-23 17:18 c9a15699
refactor(MeasureTheory/PMF): Removing `MasurableSet` hypotheses (#26230) …
4 files9 theorems
2025-06-23 17:18 c31e1e19
refactor(RingTheory/Ideal/Colon): generalize `Ideal.mem_colon_singleton` (#25850) …
1 files2 theorems
2025-06-23 16:55 285bbd05
chore: update Mathlib dependencies 2025-06-23 (#26311) …
1 files
2025-06-23 16:43 338ea157
feat: `lake exe cache` correctly detects fork from PR source (#25895) …
1 files1 defs
2025-06-23 15:53 464bf246
feat: unit space of a (locally) compact T1 monoid is (locally) compact (#26153) …
2 files3 theorems
2025-06-23 14:57 f0f62b72
feat(NumberTheory/Cyclotomic/Basic): generalize some results for cyclotomic field (#26266) …
6 files14 theorems1 defs
2025-06-23 14:42 f355283a
feat: a measurable space structure on `WithLp` (#26249) …
2 files6 theorems
2025-06-23 14:05 12808161
feat: IMO 1985 Q2 (#25783)
7 files5 theorems3 defs
2025-06-23 13:31 ddf91f15
feat: topology on `PiLp` (#26261) …
2 files2 theorems
2025-06-23 13:22 8af5157f
chore: move all nightly-testing infrastructure to a fork (#26286) …
12 files
2025-06-23 13:09 9cc0d159
feat: lemmas about orthonormal bases (#26276) …
1 files7 theorems
2025-06-23 11:31 f609d634
feat(Probability): sum of sub-Gaussian random variables is sub-Gaussian (#26164) …
2 files12 theorems
2025-06-23 10:32 ee5b18c7
chore(Tactic/ToAdditive): remove deprecated `to_additive_reorder` syntax (#26017) …
1 files
2025-06-23 09:10 8425daf3
feat: first main theorem of value distribution theory (#26093) …
6 files10 theorems
2025-06-23 08:19 df94cc8a
feat(Analysis/Normed/Operator): continuity of forming ContinuousLinearMap coproducts pointwise (#26273) …
1 files2 theorems
2025-06-23 08:19 1ad3b0ed
chore(Topology/Algebra/Semigroup): reduce import (#26257) …
1 files
2025-06-23 08:19 b38e0af9
chore: fix WithLp defeq abuse (#26248) …
1 files
2025-06-23 08:19 ee285be6
feat(RingTheory): IsPrime.one_notMem (#26203)
1 files2 theorems
2025-06-23 08:19 21f16b8e
feat(FieldTheory/IntermediateField/Algebraic): Containment of intermediate fields implies divisibility of `finrank` (#26191) …
1 files4 theorems
2025-06-23 08:19 5fbc6e5c
feat(FieldTheory/Galois/IsGaloisGroup): Remove finiteness assumption from `card_eq_finrank` (#26187) …
1 files1 theorems
2025-06-23 08:19 a7e07604
feat: T₁ iff T₀ and R₀ (#26064)
1 files2 theorems
2025-06-23 08:19 761f9b55
feat(MeasureTheory/Decomposition): link the clipped sub of positive measures to Jordan decomposition (#23500) …
5 files15 theorems1 defs1 structures
2025-06-23 07:20 f5e444c2
chore(Algebra): replace messy `simps!` with Aesop lemmas, add a test (#26127) …
5 files4 theorems
2025-06-23 00:07 7585da85
chore: correct link (#26278)
1 files
2025-06-22 22:27 dfe27eb2
style: rename `EventuallyMeasurableSpace` to `eventuallyMeasurableSpace` (#26232) …
3 files2 theorems3 defs
2025-06-22 20:25 4f1603b0
feat(CategoryTheory/Monoidal/Action): monoidal right actions (#25840) …
1 files22 theorems3 defs
2025-06-22 20:09 f29580df
refactor: deprecate module `BooleanAlgebra.lean` (#26275) …
2 files
2025-06-22 16:54 ffbf9db0
feat(CategoryTheory/Functor/KanExtension): preservations of Kan extensions (#25753) …
3 files24 theorems16 defs
2025-06-22 15:35 50a12a26
refactor: split `BooleanAlgebra` into `Basic` and `Defs` (#26173) …
9 files6 theorems2 defs
2025-06-22 14:18 27dacf78
chore: verify statements listed in 1000.yaml and similar actually exist (#26183) …
2 files
2025-06-22 12:57 57807335
chore(SimpleGraph): split `Combinatorics.SimpleGraph.Path` (#25844) …
13 files286 theorems34 defs10 structures
2025-06-22 09:40 e004dbe1
chore(CategoryTheory/MorphismProperty): the trivial property is stable under (co)base change (#26228)
1 files
2025-06-22 09:40 872fd693
feat(CategoryTheory/Extensive): pullbacks distribute over finite coproducts (#26186) …
6 files12 theorems2 defs
2025-06-22 09:31 36f34a44
chore: unprime the Prop-valued fields of `Grp_Class` (#26252) …
3 files2 theorems
2025-06-22 09:17 98757f74
doc: Fix swapped doc strings for mabs_div_lt_of_one_le_of_lt (#26262) …
1 files
2025-06-22 08:32 69f66e45
feat(CategoryTheory/Join): Pseudofunctoriality of joins of categories (#25744) …
3 files12 theorems4 defs
2025-06-22 06:18 087a0dcf
feat(Combinatorics/SimpleGraph): edgeSet of Eulerian walk equal to edgeSet of graph (#26263) …
1 files2 theorems
2025-06-22 05:59 61554979
feat(CategoryTheory/Products/Basic): alternative constructor for morphisms in products (#26206) …
6 files2 theorems
2025-06-21 12:16 e2f8bf7b
feat: specific lemmas about integrability of ContinuousMap[Zero]-valued functions (#26058) …
3 files14 theorems
2025-06-21 11:35 8f5e35a6
feat(Algebra/Star/Basic): star_mem_iff for involutive star (#25863) …
1 files1 theorems
2025-06-21 10:28 d1b53a66
feat(RingTheory/KrullDimension/PID): remove domain condition in `IsPrincipalIdealRing.krullDimLE_one` (#25728)
1 files
2025-06-21 09:33 75e445ff
chore: use `inherit_doc` in the notations for `CovBy` and `WCovBy` (#25867)
1 files
2025-06-21 09:25 17eb7da2
feat(Data/Matrix): `Matrix.fromRows_map` and `Matrix.fromCols_map` (#26222) …
1 files2 theorems
2025-06-21 01:15 c3b173fd
chore: update Mathlib dependencies 2025-06-21 (#26242) …
1 files
2025-06-20 23:24 2e2176e9
feat(SimpleGraph): Small refactor + helper lemma (#25654) …
1 files3 theorems