Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-18 07:03 8ab1a39d

View on Github →

chore(field_theory/minpoly): meaningful variable names (#5773)

Estimated changes

Modified src/field_theory/minpoly.lean

modified theorem minpoly.aeval_ne_zero_of_dvd_not_unit_minpoly

modified theorem minpoly.degree_pos

modified theorem minpoly.dvd

modified theorem minpoly.dvd_map_of_is_scalar_tower

modified theorem minpoly.eq_X_sub_C

modified theorem minpoly.eq_X_sub_C_of_algebra_map_inj

modified theorem minpoly.gcd_domain_dvd

modified theorem minpoly.gcd_domain_eq_field_fractions

modified theorem minpoly.integer_dvd

modified theorem minpoly.min

modified theorem minpoly.ne_zero

modified theorem minpoly.one

modified theorem minpoly.over_int_eq_over_rat

modified theorem minpoly.root

modified theorem minpoly.unique'

modified theorem minpoly.unique

modified theorem minpoly.zero