Commit 2024-10-21 00:31 0cfd3c80

View on Github →

chore: more fixes for multigoal linter (#17966) Preparation for #12339.

Estimated changes

Modified Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

Modified Mathlib/Analysis/SpecificLimits/RCLike.lean

Modified Mathlib/Data/Nat/Choose/Factorization.lean

Modified Mathlib/NumberTheory/Ostrowski.lean

Modified Mathlib/RingTheory/LocalRing/Quotient.lean

Modified Mathlib/RingTheory/Smooth/Pi.lean

Modified Mathlib/Topology/MetricSpace/HolderNorm.lean