Changelog

feat: small API lemma about ContinuousMap[Zero].mkD (#26250)

feat: `norm_num` plugin for `Nat.clog` (#26317)

fix(maintainer_merge_wf_run.yml): add missing AUTHOR env var (#26324) …

fix(maintainer_*_wf_run.yml): correct syntax for multiline strings (#26323) …

chore: rewrite maintainer_*.yml to work from forks (#26288) …

refactor(MeasureTheory/PMF): Removing `MasurableSet` hypotheses (#26230) …

refactor(RingTheory/Ideal/Colon): generalize `Ideal.mem_colon_singleton` (#25850) …

chore: update Mathlib dependencies 2025-06-23 (#26311) …

feat: `lake exe cache` correctly detects fork from PR source (#25895) …

feat: unit space of a (locally) compact T1 monoid is (locally) compact (#26153) …

feat(NumberTheory/Cyclotomic/Basic): generalize some results for cyclotomic field (#26266) …

feat: a measurable space structure on `WithLp` (#26249) …

feat: IMO 1985 Q2 (#25783)

feat: topology on `PiLp` (#26261) …

chore: move all nightly-testing infrastructure to a fork (#26286) …

feat: lemmas about orthonormal bases (#26276) …

feat(Probability): sum of sub-Gaussian random variables is sub-Gaussian (#26164) …

chore(Tactic/ToAdditive): remove deprecated `to_additive_reorder` syntax (#26017) …

feat: first main theorem of value distribution theory (#26093) …

feat(Analysis/Normed/Operator): continuity of forming ContinuousLinearMap coproducts pointwise (#26273) …

chore(Topology/Algebra/Semigroup): reduce import (#26257) …

chore: fix WithLp defeq abuse (#26248) …

feat(RingTheory): IsPrime.one_notMem (#26203)

feat(FieldTheory/IntermediateField/Algebraic): Containment of intermediate fields implies divisibility of `finrank` (#26191) …

feat(FieldTheory/Galois/IsGaloisGroup): Remove finiteness assumption from `card_eq_finrank` (#26187) …

feat: T₁ iff T₀ and R₀ (#26064)

feat(MeasureTheory/Decomposition): link the clipped sub of positive measures to Jordan decomposition (#23500) …

chore(Algebra): replace messy `simps!` with Aesop lemmas, add a test (#26127) …

chore: correct link (#26278)

style: rename `EventuallyMeasurableSpace` to `eventuallyMeasurableSpace` (#26232) …

feat(CategoryTheory/Monoidal/Action): monoidal right actions (#25840) …

refactor: deprecate module `BooleanAlgebra.lean` (#26275) …

feat(CategoryTheory/Functor/KanExtension): preservations of Kan extensions (#25753) …

refactor: split `BooleanAlgebra` into `Basic` and `Defs` (#26173) …

chore: verify statements listed in 1000.yaml and similar actually exist (#26183) …

chore(SimpleGraph): split `Combinatorics.SimpleGraph.Path` (#25844) …

chore(CategoryTheory/MorphismProperty): the trivial property is stable under (co)base change (#26228)

feat(CategoryTheory/Extensive): pullbacks distribute over finite coproducts (#26186) …

chore: unprime the Prop-valued fields of `Grp_Class` (#26252) …

doc: Fix swapped doc strings for mabs_div_lt_of_one_le_of_lt (#26262) …

feat(CategoryTheory/Join): Pseudofunctoriality of joins of categories (#25744) …

feat(Combinatorics/SimpleGraph): edgeSet of Eulerian walk equal to edgeSet of graph (#26263) …

feat(CategoryTheory/Products/Basic): alternative constructor for morphisms in products (#26206) …

feat: specific lemmas about integrability of ContinuousMap[Zero]-valued functions (#26058) …

feat(Algebra/Star/Basic): star_mem_iff for involutive star (#25863) …

feat(RingTheory/KrullDimension/PID): remove domain condition in `IsPrincipalIdealRing.krullDimLE_one` (#25728)

chore: use `inherit_doc` in the notations for `CovBy` and `WCovBy` (#25867)

feat(Data/Matrix): `Matrix.fromRows_map` and `Matrix.fromCols_map` (#26222) …

chore: update Mathlib dependencies 2025-06-21 (#26242) …

feat(SimpleGraph): Small refactor + helper lemma (#25654) …