Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-03 12:53 d6e1c554

View on Github →

chore(data/polynomial/monic): dedup degree_map (#11792)

Estimated changes

Modified src/data/polynomial/monic.lean

deleted theorem polynomial.degree_map'

deleted theorem polynomial.nat_degree_map'

added theorem polynomial.nat_degree_map_eq_of_injective

Modified src/field_theory/splitting_field.lean

Modified src/ring_theory/algebraic.lean

Modified src/ring_theory/polynomial/gauss_lemma.lean