Mathlib v3 is deprecated. Go to Mathlib v4

Theorem polynomial.nat_degree_add_eq_left_of_nat_degree_lt

Modification history

2021-12-31 19:13
src/data/polynomial/degree/definitions.lean
feat(data/polynomial/degree/lemmas): (nat_)degree_sum_eq_of_disjoint (#11121) …
Added polynomial.nat_degree_add_eq_left_of_nat_degree_ltView on Github →