Def PolynomialLaw.lifts

Modification history

2026-10-11 17:26
Mathlib/RingTheory/PolynomialLaw/Basic.lean
chore: use the `Finset.card` notation more widely (#44638) …
Modified PolynomialLaw.liftsView on Github →
2025-12-14 12:40
Mathlib/RingTheory/PolynomialLaw/Basic.lean
feat(RingTheory/PolynomialLaw/Basic): extends polynomial laws to arbitrary universes (#26719) …
Added PolynomialLaw.liftsView on Github →