Theorem PolynomialLaw.comp_assoc

Modification history

2025-09-26 06:18
Mathlib/RingTheory/PolynomialLaw/Basic.lean
chore(RingTheory): golf entire `coeff_opRingEquiv` and `comp_assoc` using `rfl` (#28571)
Modified PolynomialLaw.comp_assocView on Github →
2025-03-31 07:56
Mathlib/RingTheory/PolynomialLaw/Basic.lean
feat(RingTheory/PolynomialLaw/Basic): definition and elementary properties of polynomial laws (#22912) …
Added PolynomialLaw.comp_assocView on Github →