Commit 2025-10-02 05:40 18a54b03

View on Github →

chore: remove redundant generalize, induction, repeat' and unfold invocations (#29317)

Estimated changes

Modified Mathlib/Algebra/Order/Archimedean/Class.lean

Modified Mathlib/Data/ENNReal/Real.lean

Modified Mathlib/RingTheory/Polynomial/Opposites.lean

modified theorem Polynomial.support_opRingEquiv