Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-26 13:30 7d864755

View on Github →

feat(data/polynomial): eq_one_of_is_unit_of_monic (#2823) ~~Depends on #2822 ~~

Estimated changes

Modified src/data/polynomial.lean

added theorem polynomial.degree_nonneg_iff_ne_zero

added theorem polynomial.eq_one_of_is_unit_of_monic

added theorem polynomial.nat_degree_eq_zero_iff_degree_le_zero