Changelog

chore: fix docstring of `HeytingAlgebra.himp_bot` (#16587) …

chore: Move pointwise finset lemmas under `Algebra` (#16744)

chore(scripts/get_tlabel.sh): use 'CI' and 'IMO' labels for maintainer merge (#16726)

feat(Tactic/CategoryTheory/ToApp): Add `to_app` attribute (#16119) …

feat(Ergodic/Conservative): add `Conservative.measureRestrict` (#16126)

chore(LinearAlgebra): prepare library for API refactor (#16738) …

feat(CategoryTheory/Galois): generalize transitivity to arbitrary universes (#16664) …

chore: match the definition of `AnalyticWithinAt` with `ContDiffWithinAt` (#16725) …

chore: namespace lemmas to `CStarAlgebra` instead of `CStarRing` (#16653) …

feat(CategoryTheory/Abelian): AB4 and AB5 axioms (#6504) …

feat(CategoryTheory/Filtered): finality and initiality of projections on (co)structured arrow cats (#16680)

feat: lint on (syntactically) duplicate imports (#16384) …

feat: Prop-valued version of `RCLike` structure for normed fields (#16383) …

chore: deprecate 14 `Init.Logic` lemmas (#16721) …

chore: split Analysis.ContDiff.Defs into two files (#16720) …

feat(Algebra/OpenSubgroup): quotient of compact group by open subgroup is finite (#16671) …

feat(CategoryTheory/Monoidal): string diagram command (#15929) …

feat(Data/Nat/Bitwise): more symmetric statement of `Nat.xor_trichotomy` (#16693) …

chore: include LeanSearchClient in the cache (#16717)

feat: `Small.{u}` sets are closed under various operations (#11126) …

feat: generalize Module.Free.ChooseBasisIndex.fintype and Module.Finite.matrix to semirings (#16700)

feat(Combinatorics/Configuration): Projective planes over fields (#16684) …

chore: remove some unnecessary `have`s (#16659) …

feat(Order/SuccPred/Limit): `IsSuccLimit` (#16499) …

feat: improve `subst_hom_lift` macro (#16304) …

chore(SetTheory/Ordinal/Arithmetic): hide implementation details (#16703) …

feat(SetTheory/Ordinal/Basic): prove linear order instance earlier (#16401) …

feat(Algebra/Order/Archimedean/Submonoid): `SubmonoidClass.instMulArchimedean` (#16430)

feat: catch non-zero exit code from print-style-output (#16709) …

feat: #leansearch command (#16695) …

chore: deprecate all but `IsSymmOp` in `Init.Algebra.Classes` (#16698) …

chore: namespace `rsuffices` (#16708) …

chore: update Mathlib dependencies 2024-09-11 (#16714) …

fix: please the long line linter in check-yaml (#16697) …

feat(Lie): make `CommutatorRing` a `NonUnitalNonAssocRing` (#16702) …

feat(Data/Set/Finite): added lemmas about cardinality of finite sets (#15652) …

feat(GroupTheory/GroupAction/Quotient): `equivSubgroupOrbitsQuotientGroup` (#15506) …

feat(Algebra/BigOperators/Associated): add lemma divisor_closure_eq_closure (#11888) …

feat(Algebra/Polynomial/Derivation): coefficient-wise derivation on a polynomial (#14702) …

fix: make print-style-errors.sh robust against file names with quotes (#16699) …

chore: deprecate `dif_ctx_congr`, move `if_(ctx_)congr` (#16692) …

chore: remove variables from LinearAlgebra.FreeModule.Finite.Basic (#16662) …

feat: MonoidHom.div_mem_ker_iff (#16642)

feat(Algebra/BigOperators): product of MulHom over nonempty multisets (#16602)

feat(FieldTheory/{SeparableDegree|PurelyInseparable}): generalize some results on purely inseparable extension to non-commutative case (#16585) …

chore: move `ExistsUnique`, `Xor'` out of `Init.Logic` (#16691) …

feat(ModelTheory/Satisfiability): Fix universe on ModelsBoundedFormula, derive consequences for models in all universes (#16676) …

feat(Filter/Prod): add `comap_prodMap_prod` (#16564)

Revert "perf: synth order of `SMul` hierarchy (#16646)" (#16689) …

chore: make inner product notation `⟪x, y⟫_𝕜` scoped in namespace `InnerProductSpace` (#16672) …