Commit 2023-07-19 19:29 3f8ba088

View on Github →

feat: add lemmas about natDegree (#5735) Adds two lemmas about Polynomial.natDegree

Estimated changes

Modified Mathlib/Data/Polynomial/Degree/Definitions.lean

added theorem Polynomial.eq_C_coeff_zero_iff_natDegree_eq_zero

added theorem Polynomial.natDegree_C_add

added theorem Polynomial.natDegree_add_C

modified theorem Polynomial.natDegree_linear