Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-30 12:01 fed6c587

View on Github →

feat(algebra/euclidean_domain): change definition of ED and instance for polynomials (#211)

Estimated changes

Modified algebra/euclidean_domain.lean

added theorem euclidean_domain.lt_one

added theorem euclidean_domain.mod_lt

added theorem euclidean_domain.mul_right_not_lt

modified theorem euclidean_domain.val_dvd_le

deleted theorem euclidean_domain.val_le_mul_right

deleted theorem euclidean_domain.val_lt_one

deleted theorem euclidean_domain.val_mod_lt

Modified data/polynomial.lean

added theorem polynomial.degree_add_div

added theorem polynomial.degree_le_mul_left

added theorem polynomial.div_def

added theorem polynomial.div_eq_zero_iff

added theorem polynomial.mod_def

added theorem polynomial.mod_eq_self_iff