Changelog
2025-05-15 03:04 b5606ea6
chore: fix more odd indents (#24908) …
86 files3 theorems
2025-05-15 03:04 a19e5f28
feat(Algebra/Order/Ring/Unbundled/Basic): add (x - a) * (x - b) positivity criterion (#24418)
1 files4 theorems
2025-05-15 02:49 c2bce15c
feat: `a * b⁻¹` for `a b : Aˣ` is unitary if `star a * a = star b * b` (#24858)
1 files3 theorems
2025-05-14 23:43 d6c3a2d2
feat(Combinatorics): multigraphs (#24122) …
3 files44 theorems4 defs1 structures
2025-05-14 22:22 2aa8eec3
feat(Topology/Subbasis): prove Alexander Subbasis Theorem (#24856) …
1 files2 theorems
2025-05-14 19:58 909e3790
feat: restore positivity extensions for `EReal` (#24539)
1 files2 defs
2025-05-14 19:14 39b2d3e8
feat(Tactic/ToAdditive): check that existing additive declaration matches up (#24401) …
28 files25 theorems
2025-05-14 18:50 73a7031f
feature(Analysis/SpecialFunctions/Complex/CircleAddChar): ZMod.toCircle_eq_circleExp (#24463) …
1 files1 theorems
2025-05-14 18:08 5ffbd436
style: fix more doc-strings with indentation by an odd number of spaces (#24907) …
56 files
2025-05-14 17:41 70a5f9ff
style: rename `Nat.Partrec.Code.xxx_prim` to `primrec_xxx` (#24811)
2 files20 theorems
2025-05-14 16:58 2ab0f2d9
style: fix bad tactic indentation (#24890)
35 files4 theorems
2025-05-14 16:52 655d8801
chore: fix more odd indentation (#24906)
6 files
2025-05-14 16:03 c61b9b01
feat(Analysis/Normed/Unbundled/AlgNormOfAut): add algNormOfAut (#23184) …
2 files8 theorems2 defs
2025-05-14 15:37 9b1d9062
feat: the Grothendieck group of a fg monoid is fg (#24896) …
3 files2 theorems1 defs
2025-05-14 15:37 6f9d8400
feat: subspace of tychonoff space is tychonoff (#24815)
1 files2 theorems
2025-05-14 15:37 7c75d4cf
refactor: move the construction of `ChosenFiniteProducts` from finite products with `ChosenFiniteProducts` (#24679) …
5 files18 theorems3 defs
2025-05-14 14:51 846b9edd
doc(Order): replicate the Algebra subfolders design in Order (#24897) …
1 files
2025-05-14 14:51 6da103a5
chore: make sure items in docs have no odd indentation (#24893) …
70 files
2025-05-14 14:51 28cd001d
feat: a finitely generated submonoid has a minimal generating set (#23904) …
1 files2 theorems
2025-05-14 14:51 b145a856
chore: move `StrictMonoOn f s → InjOn f s` earlier (#23424) …
10 files12 theorems
2025-05-14 13:52 95bc7692
style(NumberTheory): make sure items in docs have no odd indentation (#24902) …
101 files
2025-05-14 13:52 cc3535b9
style(LinearAlgebra): make sure items in docs have no odd indentation (#24901) …
59 files
2025-05-14 13:52 8a273f31
chore: tweak output of discover-lean-pr-testing.yml (#24898)
1 files
2025-05-14 13:17 b4b5d9c8
doc(/Data/NNReal/Defs): typo (#24895) …
1 files
2025-05-14 13:17 02065d27
feat: minimal elements exist in well-founded orders (#24766) …
1 files6 theorems
2025-05-14 13:17 179655ba
refactor: use a junk value for the analytic order of a non-analytic function (#22974) …
6 files54 theorems
2025-05-14 12:37 88c66491
chore: use TreeMap in linarith Fourier-Motzkin oracle (#24903) …
2 files
2025-05-14 12:37 79c1c03f
feat: `s \ {a ∈ s | p a} = {a ∈ s | ¬ p a}` (#24888) …
1 files1 theorems
2025-05-14 11:30 624a3531
chore(Algebra): make sure items in docs have no odd indentation (#24886) …
47 files
2025-05-14 10:52 f55ac5ea
refactor: spell results using `Minimal`/`MinimalFor` (#23487) …
21 files44 theorems
2025-05-14 10:34 37c01f2e
feat(RingTheory/PowerSeries/Substitution): define substitution of power series in power series (#23552) …
4 files52 theorems
2025-05-14 09:23 bdbaaec4
feat(GroupTheory/GroupAction/Basic): equivalences between stabilizers (#24107) …
2 files13 theorems2 defs
2025-05-14 09:01 28f339a6
feat: basic `InfinitePlace.comap` lemmas (#24879)
1 files2 theorems
2025-05-14 08:44 c53aaa67
feat(Algebra/Ring): associator of a non-associative ring (#22823) …
3 files11 theorems4 defs
2025-05-14 07:47 274edf8a
chore: add deprecations for {Extract,Lift}Lets.lean (#24871) …
4 files
2025-05-14 07:47 753ef7e3
feat: more lemmas about torsion-free monoids (#24312) …
9 files8 theorems
2025-05-14 07:02 6534503f
chore: fix some indentation (#24874)
4 files
2025-05-14 04:50 1bd7adb3
chore(SimpleFuncDense): minimise opens and variables (#24863) …
1 files
2025-05-13 23:40 40fea086
feat: promote `mem_unitary_of_star_mul_self` to an `Iff` (#24867)
1 files4 theorems
2025-05-13 23:15 21258ca7
fix: add a space to the pretty printer for `deprecated_module` (#24864) …
1 files
2025-05-13 22:40 7ae6f6a7
feat(Topology/Algebra/InfiniteSum): uniform summability (#23507) …
4 files22 theorems4 defs
2025-05-13 22:31 68321034
feat(AlgebraicGeometry): sigma functor on covers (#24723)
3 files
2025-05-13 21:42 9eecc5f5
chore(CategoryTheory/Idempotents): fix simp direction in Karoubi (#24848)
2 files1 theorems
2025-05-13 21:29 87a50461
chore: fix spelling mistakes (#24857)
7 files
2025-05-13 20:30 22030a26
feat(CategoryTheory/Limits/Final): `fromPUnit c` is final if `c` is terminal (#24847) …
3 files4 theorems
2025-05-13 18:29 e9db98be
feat(Data/Finsupp/MonomialOrder): give `≼[m]`/ `≺[m]` the same priority as `≤`/`<` (#24832) …
1 files
2025-05-13 18:00 440abb3d
chore: whitespace adaptations (#24854) …
2 files4 theorems
2025-05-13 17:38 bce1d651
feat: `x ∉ span R s` if `insert x s` is linearly independent (#24852) …
3 files7 theorems
2025-05-13 16:40 400dde68
feat(Topology): subspace of quotient topology is quotient of subspace topology (#23527)
1 files3 theorems
2025-05-13 16:33 f372074b
feat(Topology/MetricSpace): pseudometrics as bundled functions (#23111) …
2 files12 theorems1 structures