Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-09 11:28 c4a34136

View on Github →

chore(data/polynomial): use dot notation for monic lemmas (#12530) As discussed in #12447

Use the notation throughout the library
Also deleted ne_zero_of_monic as it was a duplicate of monic.ne_zero it seems.
Cleaned up a small proof here and there too.

Estimated changes

Modified src/data/polynomial/div.lean

Modified src/data/polynomial/lifts.lean

modified theorem polynomial.lifts_and_degree_eq_and_monic

Modified src/data/polynomial/monic.lean

deleted theorem polynomial.degree_map_of_monic

added theorem polynomial.monic.add_of_left

added theorem polynomial.monic.add_of_right

added theorem polynomial.monic.degree_map

added theorem polynomial.monic.map

added theorem polynomial.monic.mul

added theorem polynomial.monic.nat_degree_map

added theorem polynomial.monic.pow

modified theorem polynomial.monic_C_mul_of_mul_leading_coeff_eq_one

deleted theorem polynomial.monic_add_of_left

deleted theorem polynomial.monic_add_of_right

deleted theorem polynomial.monic_map

deleted theorem polynomial.monic_mul

modified theorem polynomial.monic_mul_C_of_leading_coeff_mul_eq_one

deleted theorem polynomial.monic_pow

deleted theorem polynomial.nat_degree_map_of_monic

deleted theorem polynomial.ne_zero_of_monic

Modified src/data/polynomial/ring_division.lean

Modified src/field_theory/minpoly.lean

Modified src/field_theory/splitting_field.lean

Modified src/ring_theory/integral_closure.lean

Modified src/ring_theory/norm.lean

Modified src/ring_theory/polynomial/basic.lean

Modified src/ring_theory/polynomial/cyclotomic/basic.lean

Modified src/ring_theory/polynomial/eisenstein.lean

Modified src/ring_theory/power_basis.lean

Modified src/ring_theory/trace.lean