Commit 2025-04-09 16:53 08976833

View on Github →

chore: miscellaneous style fixes (#23878) Prompted by the linter in #22760.

Estimated changes

Modified Mathlib/Algebra/Group/Pointwise/Finset/BigOperators.lean

modified theorem Finset.coe_prod

Modified Mathlib/Algebra/Polynomial/ofFn.lean

modified theorem Polynomial.ofFn_comp_toFn_eq_id_of_natDegree_lt

Modified Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Basic.lean

modified theorem hasFDerivAtFilter_intCast

modified theorem hasFDerivAtFilter_natCast

modified theorem hasFDerivAtFilter_ofNat

modified theorem hasFDerivAtFilter_one

modified theorem hasFDerivWithinAt_intCast

modified theorem hasFDerivWithinAt_natCast

modified theorem hasFDerivWithinAt_ofNat

modified theorem hasFDerivWithinAt_one

Modified Mathlib/CategoryTheory/Core.lean

Modified Mathlib/CategoryTheory/Discrete/SumsProducts.lean

Modified Mathlib/CategoryTheory/Sums/Basic.lean

Modified Mathlib/Data/LocallyFinsupp.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/PolarCoord.lean

modified theorem NumberField.mixedEmbedding.normAtComplexPlaces_polarSpaceCoord_symm

Modified Mathlib/RingTheory/PolynomialLaw/Basic.lean

Modified Mathlib/Topology/Algebra/UniformField.lean

Modified Mathlib/Topology/Homotopy/Lifting.lean