Commit 2025-11-03 21:57 a79df06b

View on Github →

chore: tidy various files (#31207)

Estimated changes

Modified Mathlib/Algebra/Homology/DerivedCategory/Ext/Linear.lean

Modified Mathlib/Algebra/Order/Star/Basic.lean

Modified Mathlib/Algebra/SkewMonoidAlgebra/Lift.lean

Modified Mathlib/Algebra/SkewPolynomial/Basic.lean

modified theorem SkewPolynomial.monomial_zero_one

Modified Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/IsUniquelyCodimOneFace.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean

Modified Mathlib/Analysis/Calculus/IteratedDeriv/ConvergenceOnBall.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

Modified Mathlib/Analysis/Fourier/AddCircle.lean

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Abs.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Opposites/Equalizers.lean

Modified Mathlib/Combinatorics/Enumerative/Bell.lean

Modified Mathlib/Control/Monad/Cont.lean

Modified Mathlib/GroupTheory/FreeGroup/Orbit.lean

Modified Mathlib/MeasureTheory/Measure/HasOuterApproxClosedProd.lean

Modified Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean

Modified Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean

Modified Mathlib/RepresentationTheory/Homological/FiniteCyclic.lean

Modified Mathlib/RepresentationTheory/Homological/GroupHomology/FiniteCyclic.lean

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

Modified Mathlib/RingTheory/LaurentSeries.lean

Modified Mathlib/RingTheory/WittVector/TeichmullerSeries.lean

Modified Mathlib/Topology/Algebra/Order/ArchimedeanDiscrete.lean

Modified Mathlib/Topology/Algebra/ProperAction/Basic.lean

Modified Mathlib/Topology/Convenient/GeneratedBy.lean