Changelog

2025-07-16 01:19 488d3b8e
chore: fix four `Submonoid` recursors (#27185) …
3 files4 theorems
2025-07-15 22:37 3a074087
chore: import `rw??` into `Mathlib.Tactic.Common` (#27164) …
2 files
2025-07-15 21:51 42632e67
feat(NumberTheory/Padics/ValuativeRel): ValuativeRel ℚ_[p] (#27177) …
3 files2 theorems
2025-07-15 19:54 5bfba479
feat: solution to ODE is Lipschitz with respect to the initial condition (#26392) …
1 files6 theorems
2025-07-15 19:38 54b59e30
chore: generalise `FreeGroup.ext_hom` to monoids (#27140) …
1 files1 theorems
2025-07-15 17:59 e2292a32
feat(CategoryTheory/Adjunction): the right partial adjoint (#27168) …
1 files9 theorems1 defs
2025-07-15 17:23 845ff2b8
feat(Data/Matrix): add `Matrix.vecCons_inj` (#26896) …
2 files1 theorems
2025-07-15 16:28 3e077d83
feat: Finset.max'_eq_iff (#27153) …
1 files2 theorems
2025-07-15 16:05 ccca4728
feat(CategoryTheory/Preadditive/Injective/Basic, CategoryTheory/Preadditive/Projective/Basic): injectivity/projectivity criterion (#27156) …
2 files2 theorems
2025-07-15 14:02 4940ad6e
feat(Algebra/SkewMonoidAlgebra/Basic): multiplication and algebraic instances (#26933) …
1 files29 theorems8 defs
2025-07-15 13:39 efb60912
feat(Algebra/Polynomial/AlgebraMap): add lemmas (#26666)
2 files4 theorems2 defs
2025-07-15 12:22 e87547a2
chore: golf Algebra/ using `simp`/`simp_all` (#27130)
21 files
2025-07-15 11:35 f96ef6f7
feat: add Mathlib.RingTheory.DedekindDomain.Instances (#26070) …
12 files6 theorems
2025-07-15 10:52 b330acfb
feat: coin problem with two coins and prime ideals in ℕ (#27065) …
7 files12 theorems
2025-07-15 10:09 a806dee0
feat: `Finset.mem_filter_univ` (#27148) …
25 files1 theorems
2025-07-15 10:09 a5d42804
feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): bicategory-like lemmas for `CatCospanTransforms` (#26447) …
1 files14 theorems
2025-07-15 09:22 6c0e8529
chore: remove whitespace (#26963) …
40 files5 theorems
2025-07-15 08:53 6b9514a6
feat(Topology/GDelta/Basic): two basic lemmas about unions of meagre sets (#26979) …
1 files4 theorems
2025-07-15 08:53 db444811
chore: golf CategoryTheory/ using `grind` (#26691)
5 files
2025-07-15 08:52 40b305cc
feat(CategoryTheory/Topos): subobject classifier without limits (#26556) …
3 files10 theorems2 defs
2025-07-15 08:52 3d1fc475
fix(Topology/Covering): switch to standard definition (#24983) …
3 files14 theorems
2025-07-15 08:52 f68e1d93
chore(Topology.MetricSpace.Lipschitz): stop depending on Topology.Algebra (#23498) …
9 files6 theorems
2025-07-15 08:11 341594fa
feat: characterise membership in `SO(2)` (#27121) …
1 files4 theorems
2025-07-15 08:11 4627273f
feat(Algebra/GroupWithZero/Range): MonoidWithZeroHom.(m)range_nontrivial (#27114) …
1 files2 theorems
2025-07-15 08:11 1164c0de
feat: semilinearize `LinearEquiv.conjRingEquiv` (#27104)
3 files13 theorems5 defs
2025-07-15 08:11 11385264
refactor(LinearAlgebra/LinearIndependent): generalize some `LinearIndepOn` theorems (#27096) …
2 files10 theorems
2025-07-15 08:11 de0a2931
doc(Algebra/Homology/Homotopy): add field docstrings to `HomotopyEquiv` (#27048) …
1 files
2025-07-15 08:11 e7670e56
chore(Analysis/InnerProductSpace/Projection): deprecating `subtypeL ∘ orthogonalProjection` in favor of `starProjection` (#26877) …
6 files51 theorems
2025-07-15 08:11 78257c27
chore: golf RingTheory/ using `grind` (#26698)
1 files
2025-07-15 08:10 d660e92a
chore: golf LinearAlgebra/ using `grind` (#26685)
8 files
2025-07-15 08:10 09161bde
chore: golf GroupTheory/ using `grind` (#26681)
5 files
2025-07-15 08:10 59c80bca
feat: equivalent condition for subgroups to be simple (#26552) …
2 files2 theorems
2025-07-15 08:10 d0f1801b
feat(AlgebraicTopology): cylinder objects in model categories (#26171) …
5 files10 theorems2 defs2 structures
2025-07-15 08:10 42d7516d
feat(Aesop): Improve SetLike ruleset (#25961) …
15 files3 theorems
2025-07-15 08:10 92dbb752
chore: rename arguments to `Matrix.submatrix` (#24883) …
2 files3 theorems1 defs
2025-07-15 07:59 3c104899
chore: golf AlgebraicGeometry/ using `grind` (#26695)
3 files
2025-07-14 23:31 507dd92b
feat: add instance `CanonicallyOrderedAdd` for `Ordinal` (#27145)
2 files
2025-07-14 21:16 0bf25725
chore(Algebra): replace CoeFun.coe with DFunLike.coe (#27146)
1 files1 theorems
2025-07-14 21:16 d354aa91
chore: replace `DFunLike` → `FunLike` if possible (#27144) …
4 files
2025-07-14 21:15 15b41842
chore(RingTheory/ValuationSubring): valuationSubring_integers (#27111) …
1 files1 theorems
2025-07-14 20:27 9aeee99d
feat: Subtype.map_{eq,ne} (#27012)
1 files2 theorems
2025-07-14 16:30 5338f341
feat(CategoryTheory): `inv (μ F X Y) = δ F X Y` (#27061) …
2 files15 theorems
2025-07-14 15:57 6f9f6ef0
feat(LinearAlgebra/Finsupp/LinearCombination): add `Submodule.mem_span_finset'` (#27097) …
1 files1 theorems
2025-07-14 15:13 f68fe3b9
feat: `(vecMulVec _ _).rank ≤ 1` (#27075) …
4 files3 theorems
2025-07-14 14:29 94d81ee4
refactor: deprecate `sSup_le_sSup_of_forall_exists_le` in `CompleteLattice` in favor of `sSup_le_sSup_of_isCofinalFor` (#27124) …
4 files2 theorems
2025-07-14 12:58 958ad8be
refactor(Analysis/Convex/Mul): generalize the domain of functions (#27002) …
1 files
2025-07-14 12:58 bca1e1d8
feat(Mathlib/Order/PartialSups): add `PartialSups` composition lemma (#26848) …
1 files1 theorems
2025-07-14 12:58 da48ff78
feat(Data/ENNReal): Add `sub_lt_iff_lt_left` and similar lemmas (#26815) …
1 files2 theorems
2025-07-14 12:58 94a359f9
fix(Logic/Function/Basic): change precedence of uncurry prefix operator to max (#26742) …
9 files
2025-07-14 12:29 3f20efc5
feat: inequalities for `(P ↓∩ Q).encard` (#27093) …
1 files2 theorems