Changelog

doc: add oeis attributes (#44370) …

chore: remove unnecessary set_option lines (#45012) …

fix(Tactic/CategoryTheory/Slice): do not generate redundant goals (#44569) …

feat(RingTheory/Ideal/Colon): add `colon_eq_top_iff_le` (#44965) …

feat(MvPolynomial): ideal generated by indeterminates in a polynomial ring over a domain is prime (#41399)

chore(Translate/Core): remove `allowAutoName` configuration option (#44977) …

chore(MathlibTest): remove `mkDocComment` (#44972) …

feat(ModularForms/SlashActions): more theorems for slash actions (sub,pow,zpow,inv) (#44356)

doc(Topology): update documentation to match variable name in code (#44987)

feat(RingTheory/FractionalIdeal): add HasUniqueRoots instance (#40636) …

feat(RingTheory/Valuation): valuation of an algebraic element (#40197) …

feat(Category/Abelian/Injective): interaction between `InjectiveResolution.extMk` and the connecting morphism (#43224) …

feat(Algebra/BigOperators): add theorems about prod of rotate of list (#44953) …

chore(scripts): update nolints.json (#44984) …

chore(CategoryTheory/Monad): use `to_dual` (#44628) …

chore: remove `WittVector.mk'` (#43374) …

feat: lemmas for subgroups of finite index (#44957)

feat: add QuotientGroup.instHasUniqueRoots (#44838) …

chore(Order/DirSupClosed): fix badly named theorems (#44974) …

feat(Combinatorics/SimpleGraph/Metric): add distance lemmas for graph maps (#44872) …

chore: link bors's dashboard at bors.mathlib.org (#44805) …

feat(Linter/Style): lint against `∀ᵉ`/`∃ᵉ` (#44544) …

feat(NumberTheory/EllipticDivisibilitySequence): prove that a normalised elliptic divisibility sequence is an elliptic sequence (#42453) …

feat(Geometry/Euclidean/Angle/Incenter): distance from second intersection with circumcircle (#32294) …

chore: reorder mvfderiv lemmas (#43987) …

feat(Combinatorics/SimpleGraph/Acyclic): a graph is a tree iff it's acyclic and has exactly `n - 1` edges (#34910)

chore: rename `smooth_barycentric_coord` to `contDiff_barycentric_coord` (#44960) …

ci: add `--add-public-downstream` to `shake` options (#44962) …

chore(GroupTheory/Solvable): to_additivize file (#43108) …

feat(Algebra/Order/Floor): floor-of-sum dichotomy via fractional parts (#41861) …

feat: `Finset.exists_mem_cons` (#44919) …

chore(RingTheory/IntegralClosure/IsIntegralClosure): fix instance name capitalization (#44753) …

refactor(Analysis/Convex/Caratheodory): refactor Caratheodory's theorem using strong induction (#44863) …

feat(Data/Nat/ModEq): add congruence mod lcm lemma (#44839) …

chore(MathlibTest/Linter/DupNamespace): use the module system (#44622) …

feat(Geometry/Euclidean): dist with affineCombination on one side (#44102) …

chore(RingTheory/Pochhammer): fix the type of ascPochhammer_eval_succ (#42827) …

chore(RingTheory): delete outdated `proof_wanted` (#42649) …

feat(RingTheory/QuadraticAlgebra): trace, norm and discriminant as `Algebra` invariants (#42297) …

feat(SimpleGraph): reduce CycleGraph imports (#41306) …

chore(LinearAlgebra/AffineSpace/Homogenization): use `inferInstanceAs` (#44947) …

chore: rename HomeomorphClass.toHomeomorph projection (#44907) …

feat(Analysis/Matrix/GelfandRadius): prove `gelfandRadius (A * B) = gelfandRadius (B * A)` for matrices (#44891) …

feat: every element is between two others in a club set (#44793) …

feat(Data/List): add `List.IsChain.iterate` and `List.getLast_iterate` (#44661) …

feat(SetTheory/Ordinal): classify exponential principal ordinals (#43633) …

feat(FreeGroup): characterize commutative/cyclic free groups (#41988) …

refactor: `isUpperSet_Ixi` → `IsUpperSet.Ixi` (#44929)

feat(Algebra/Field/Subfield): `Subfield.isMulCommutative_closure` (#44921) …

chore: rename `toContinuousMap` to `ContinuousMap.ofClass` (#44877) …