Commit 2025-09-26 06:18 453f2741

View on Github →

chore(RingTheory): golf entire coeff_opRingEquiv and comp_assoc using rfl (#28571)

Estimated changes

Modified Mathlib/RingTheory/FractionalIdeal/Extended.lean

modified theorem FractionalIdeal.mem_extended_iff

Modified Mathlib/RingTheory/Polynomial/Opposites.lean

Modified Mathlib/RingTheory/PolynomialLaw/Basic.lean

modified theorem PolynomialLaw.comp_assoc