Commit 2023-03-29 05:49 abf03ca7

View on Github →

feat: port Data.Polynomial.Degree.CardPowDegree (#3134)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/Degree/CardPowDegree.lean

added theorem Polynomial.cardPowDegree_apply

added theorem Polynomial.cardPowDegree_isEuclidean

added theorem Polynomial.cardPowDegree_nonzero

added theorem Polynomial.cardPowDegree_zero