Changelog

feat(Algebra/Lie): a Lie algebra is solvable iff it is solvable after faithfully flat base change (#20808)

feat: define bases of root pairings (#20667)

feat(Tactic): basic ConcreteCategory support for elementwise (#20811) …

feat(CategoryTheory): define unbundled `ConcreteCategory` class (#20810) …

chore(CategoryTheory): rename `ConcreteCategory` to `HasForget` (#20809) …

feat: `CommSemiring (NonemptyInterval ℚ≥0)` (#20783) …

chore(yaml_check.py): re-format (#20807) …

feat: elementary estimate for Real.log (#20766) …

feat: definition of linear topologies (#14990) …

feat(RingTheory): flatness over a semiring (#19115) …

feat(Algebra/Homology/Embedding): the canonical truncation truncLE (#19550) …

feat(Algebra/Homology/Embedding): API for the homology of an extension of homological complex (#19203) …

feat(Algebra/Ring): `RingEquiv.piUnique` (#20794) …

feat(RingTheory/LocalRing): add instance `Unique (MaximalSpectrum R)` for a local ring `R` (#20801) …

chore(GroupExtension/Defs): define `Section` and redefine `Splitting` (#20802) …

chore: restore `def` to `adicCompletion` (#20796) …

refactor: rename `UniqueContinuousFunctionalCalculus` to `ContinuousMap.UniqueHom` (#20643) …

feat(Algebra/Homology/Embedding): the morphism from a complex to its `truncGE` truncation (#19544) …

chore(Mathlib/Computability/TuringMachine): split file (#20790) …

feat(Data/Finset/Card): add `InjOn` and `SurjOn` versions of finset cardinality lemmas (#20753) …

feat(Order/WellFoundedSet): add convenience constructors for IsWF and IsPWO for WellFoundedLT types (#20752) …

feat(Set/Finite): a set is finite if its image and fibers are finite (#20751) …

chore: cleanup .gitignore files (#20795)

feat(Topology/Group/Profinite): Profinite group is limit of finite group (#16992) …

feat(Combinatorics/SimpleGraph): vertices in cycles (#20602) …

CI: merge `bot_fix_style` actions (#20789) …

chore: survey of simp porting notes (#20787) …

style: correct `MaximalSpectrum.IsMaximal` for style conformance. (#20792) …

feat: split Mathlib/Algebra/Order/Ring/Unbundled/Nonneg (#20703) …

refactor: make `CanonicallyOrdered...` mixin (#17444) …

feat: generalise `PerfectPairing.restrictScalarsField` (#20442) …

feat: replace statement that specific functions are C^ω by the fact that they are C^n for all n (#20769) …

feat(Algebra/Ring): generalise and extend material about sums of squares and semireal rings (#16094) …

fix(PR summary): use a file to store possibly long messages (#20761) …

chore: move Algebra/Group/ZeroOne/ to Data/ (#20622) …

refactor: move files from `AlgebraicGeometry/PrimeSpectrum` to `RingTheory/Spectrum/Prime` (#20778) …

chore: split file `LinearAlgebra.PerfectPairing` (#20780) …

chore: typos in Fderiv instead of FDeriv (#20775)

chore(Algebra/Group/Equiv): split into `Defs` and `Basic` (#20712) …

feat(ModularForms/QExpansion): define q-expansions (#20720) …

chore: fix some slow maxHeartbeats and backwards compatibility flags (#20214) …

chore: remove last few instances of `set_option tactic.skipAssignedInstances false` (#20193) …

refactor: redefine `Subrel` in terms of `α → Prop` instead of `Set α` (#20475) …

feat(Order/Interval/Finset): map sectL and sectR on finset intervals (#20759) …

chore: generalize more materials about linear independence over semirings (#20497) …

chore(Data/Fin/Basic): remove mention of `Fin.succAboveCases` (#20770) …

feat(LinearAlgebra/ExteriorPower): the pairing between the exterior power of the dual and the exterior power (#18651) …

feat(Order/Chain): condition for the union of chains to be a chain (#20758) …

refactor: split `RingTheory/{Prime,Maximal}Spectrum` into `RingTheory/Spectrum/{Prime,Maximal}/{Defs,Basic}` (#20772) …

feat: establish integrability and integrals of Real.log on arbitrary intervals (#20682) …