Theorem PolynomialLaw.toFun_eq_rTensor_φ_toFun'

Modification history

2025-12-14 12:40
Mathlib/RingTheory/PolynomialLaw/Basic.lean
feat(RingTheory/PolynomialLaw/Basic): extends polynomial laws to arbitrary universes (#26719) …
Added PolynomialLaw.toFun_eq_rTensor_φ_toFun'View on Github →