Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-12 15:42 1db04677

View on Github →

feat(data/polynomial): adjoin_root.mk_ne_zero lemmas (#18113)

mk_ne_zero_of_(nat_)degree_lt: if f : R[X] is monic and g : R[X] is nonzero with (nat_)degree less than (nat_)degree of f, then the image of g in R[X]/(f) is nonzero. Depends on new lemmas monic.not_dvd_of_(nat_)degree_lt.
Use it to golf weierstrass_curve.X/Y_class_ne_zero.
Move misplaced lemma nat_degree_lt_nat_degree.

Estimated changes

Modified src/algebraic_geometry/elliptic_curve/weierstrass.lean

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

added theorem polynomial.nat_degree_lt_nat_degree

Modified src/data/polynomial/monic.lean

modified theorem polynomial.monic.degree_le_zero_iff_eq_one

modified theorem polynomial.monic.degree_mul_comm

modified theorem polynomial.monic.nat_degree_eq_zero_iff_eq_one

modified theorem polynomial.monic.nat_degree_mul'

modified theorem polynomial.monic.nat_degree_mul

modified theorem polynomial.monic.nat_degree_mul_comm

modified theorem polynomial.monic.next_coeff_mul

added theorem polynomial.monic.not_dvd_of_degree_lt

added theorem polynomial.monic.not_dvd_of_nat_degree_lt

Modified src/ring_theory/adjoin_root.lean

added theorem adjoin_root.mk_eq_zero

added theorem adjoin_root.mk_ne_zero_of_degree_lt

added theorem adjoin_root.mk_ne_zero_of_nat_degree_lt

Modified src/ring_theory/power_basis.lean

deleted theorem power_basis.nat_degree_lt_nat_degree