Changelog

chore: fix more odd indents (#24908) …

feat(Algebra/Order/Ring/Unbundled/Basic): add (x - a) * (x - b) positivity criterion (#24418)

feat: `a * b⁻¹` for `a b : Aˣ` is unitary if `star a * a = star b * b` (#24858)

feat(Combinatorics): multigraphs (#24122) …

feat(Topology/Subbasis): prove Alexander Subbasis Theorem (#24856) …

feat: restore positivity extensions for `EReal` (#24539)

feat(Tactic/ToAdditive): check that existing additive declaration matches up (#24401) …

feature(Analysis/SpecialFunctions/Complex/CircleAddChar): ZMod.toCircle_eq_circleExp (#24463) …

style: fix more doc-strings with indentation by an odd number of spaces (#24907) …

style: rename `Nat.Partrec.Code.xxx_prim` to `primrec_xxx` (#24811)

style: fix bad tactic indentation (#24890)

chore: fix more odd indentation (#24906)

feat(Analysis/Normed/Unbundled/AlgNormOfAut): add algNormOfAut (#23184) …

feat: the Grothendieck group of a fg monoid is fg (#24896) …

feat: subspace of tychonoff space is tychonoff (#24815)

refactor: move the construction of `ChosenFiniteProducts` from finite products with `ChosenFiniteProducts` (#24679) …

doc(Order): replicate the Algebra subfolders design in Order (#24897) …

chore: make sure items in docs have no odd indentation (#24893) …

feat: a finitely generated submonoid has a minimal generating set (#23904) …

chore: move `StrictMonoOn f s → InjOn f s` earlier (#23424) …

style(NumberTheory): make sure items in docs have no odd indentation (#24902) …

style(LinearAlgebra): make sure items in docs have no odd indentation (#24901) …

chore: tweak output of discover-lean-pr-testing.yml (#24898)

doc(/Data/NNReal/Defs): typo (#24895) …

feat: minimal elements exist in well-founded orders (#24766) …

refactor: use a junk value for the analytic order of a non-analytic function (#22974) …

chore: use TreeMap in linarith Fourier-Motzkin oracle (#24903) …

feat: `s \ {a ∈ s | p a} = {a ∈ s | ¬ p a}` (#24888) …

chore(Algebra): make sure items in docs have no odd indentation (#24886) …

refactor: spell results using `Minimal`/`MinimalFor` (#23487) …

feat(RingTheory/PowerSeries/Substitution): define substitution of power series in power series (#23552) …

feat(GroupTheory/GroupAction/Basic): equivalences between stabilizers (#24107) …

feat: basic `InfinitePlace.comap` lemmas (#24879)

feat(Algebra/Ring): associator of a non-associative ring (#22823) …

chore: add deprecations for {Extract,Lift}Lets.lean (#24871) …

feat: more lemmas about torsion-free monoids (#24312) …

chore: fix some indentation (#24874)

chore(SimpleFuncDense): minimise opens and variables (#24863) …

feat: promote `mem_unitary_of_star_mul_self` to an `Iff` (#24867)

fix: add a space to the pretty printer for `deprecated_module` (#24864) …

feat(Topology/Algebra/InfiniteSum): uniform summability (#23507) …

feat(AlgebraicGeometry): sigma functor on covers (#24723)

chore(CategoryTheory/Idempotents): fix simp direction in Karoubi (#24848)

chore: fix spelling mistakes (#24857)

feat(CategoryTheory/Limits/Final): `fromPUnit c` is final if `c` is terminal (#24847) …

feat(Data/Finsupp/MonomialOrder): give `≼[m]`/ `≺[m]` the same priority as `≤`/`<` (#24832) …

chore: whitespace adaptations (#24854) …

feat: `x ∉ span R s` if `insert x s` is linearly independent (#24852) …

feat(Topology): subspace of quotient topology is quotient of subspace topology (#23527)

feat(Topology/MetricSpace): pseudometrics as bundled functions (#23111) …