Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-27 22:50 c53f9f17

View on Github →

refactor(algebra/euclidean_domain): clean up proofs

Estimated changes

Modified algebra/euclidean_domain.lean

added theorem euclidean_domain.div_add_mod

modified theorem euclidean_domain.div_self

deleted theorem euclidean_domain.dvd_mod

added theorem euclidean_domain.dvd_mod_iff

deleted theorem euclidean_domain.dvd_mod_self

modified theorem euclidean_domain.gcd.induction

deleted theorem euclidean_domain.gcd_decreasing

modified theorem euclidean_domain.gcd_dvd

added theorem euclidean_domain.gcd_eq_left

deleted theorem euclidean_domain.gcd_next

added theorem euclidean_domain.gcd_val

added theorem euclidean_domain.mod_eq_zero

deleted theorem euclidean_domain.mod_lt

modified theorem euclidean_domain.mod_zero

added theorem euclidean_domain.mul_div_cancel

added theorem euclidean_domain.mul_div_cancel_left

deleted theorem euclidean_domain.neq_zero_lt_mod_lt

added theorem euclidean_domain.val_le_mul_right

added theorem euclidean_domain.val_mod_lt

modified theorem euclidean_domain.zero_div

Modified analysis/topology/infinite_sum.lean

Modified linear_algebra/multivariate_polynomial.lean

deleted theorem finsupp.single_induction_on