Commit 2023-03-08 08:14 beaa0d2b

View on Github →

feat: port Data.Polynomial.Monomial (#2623)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/Monomial.lean

added theorem Polynomial.card_support_le_one_iff_monomial

added theorem Polynomial.monomial_one_eq_iff

added theorem Polynomial.ringHom_ext'

added theorem Polynomial.ringHom_ext