Commit 2025-02-07 14:22 8164b505

View on Github →

chore: tidy various files (#21475)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Fin.lean

Modified Mathlib/Algebra/FreeMonoid/Basic.lean

Modified Mathlib/Algebra/Homology/Embedding/Basic.lean

Modified Mathlib/Algebra/Homology/QuasiIso.lean

modified theorem HomologicalComplex.mem_quasiIso_iff

Modified Mathlib/Algebra/MonoidAlgebra/Division.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

modified theorem AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ

Modified Mathlib/Analysis/Analytic/Basic.lean

modified theorem FormalMultilinearSeries.radius_smul_eq

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean

Modified Mathlib/Data/Finset/Filter.lean

Modified Mathlib/Data/Finset/Lattice/Fold.lean

Modified Mathlib/Data/Finsupp/Lex.lean

Modified Mathlib/Data/Multiset/Range.lean

Modified Mathlib/Data/Quot.lean

Modified Mathlib/GroupTheory/Coxeter/Basic.lean

Modified Mathlib/GroupTheory/Coxeter/Inversion.lean

Modified Mathlib/GroupTheory/GroupAction/Blocks.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean

Modified Mathlib/MeasureTheory/Measure/RegularityCompacts.lean

Modified Mathlib/NumberTheory/FLT/Polynomial.lean

Modified Mathlib/RingTheory/MvPolynomial/Groebner.lean

Modified Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

Modified Mathlib/RingTheory/MvPowerSeries/PiTopology.lean

Modified Mathlib/RingTheory/Polynomial/HilbertPoly.lean

Modified Mathlib/RingTheory/RootsOfUnity/Complex.lean

Modified Mathlib/RingTheory/Smooth/Local.lean