Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-05 00:22 2d370e9d

View on Github →

feat(algebra/euclidean_domain): euclidean domains / euclidean algorithm

Estimated changes

Created algebra/euclidean_domain.lean

added theorem euclidean_domain.div_self

added theorem euclidean_domain.dvd_gcd

added theorem euclidean_domain.dvd_mod

added theorem euclidean_domain.dvd_mod_self

added theorem euclidean_domain.gcd.induction

added def euclidean_domain.gcd

added theorem euclidean_domain.gcd_decreasing

added theorem euclidean_domain.gcd_dvd

added theorem euclidean_domain.gcd_dvd_left

added theorem euclidean_domain.gcd_dvd_right

added theorem euclidean_domain.gcd_next

added theorem euclidean_domain.gcd_one_left

added theorem euclidean_domain.gcd_self

added theorem euclidean_domain.gcd_zero_left

added theorem euclidean_domain.gcd_zero_right

added theorem euclidean_domain.mod_lt

added theorem euclidean_domain.mod_one

added theorem euclidean_domain.mod_self

added theorem euclidean_domain.mod_zero

added theorem euclidean_domain.neq_zero_lt_mod_lt

added theorem euclidean_domain.val_dvd_le

added theorem euclidean_domain.val_lt_one

added theorem euclidean_domain.zero_div

added theorem euclidean_domain.zero_mod