Commit 2021-03-11 13:28 57fda28f

View on Github →

refactor(data/polynomial/degree/definitions): Remove hypothesis of nat_degree_X_pow_sub_C (#6628) The lemma nat_degree_X_pow_sub_C had an unnecessary hypothesis.

Estimated changes

Modified src/data/polynomial/degree/definitions.lean

modified theorem polynomial.nat_degree_X_pow_sub_C

Modified src/ring_theory/polynomial/cyclotomic.lean