Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-23 09:33 69485051

View on Github →

feat(data/polynomial): prime_of_degree_eq_one_of_monic (#2745)

Estimated changes

Modified src/data/polynomial.lean

added theorem polynomial.degree_normalize

added theorem polynomial.irreducible_of_degree_eq_one_of_monic

added theorem polynomial.prime_of_degree_eq_one

added theorem polynomial.prime_of_degree_eq_one_of_monic