Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-18 17:14 0854e839

View on Github →

chore(algebra/euclidean_domain): docstrings (#3816)

Estimated changes

Modified src/algebra/euclidean_domain.lean

modified theorem euclidean_domain.div_add_mod

modified theorem euclidean_domain.div_self

modified theorem euclidean_domain.div_zero

modified theorem euclidean_domain.dvd_gcd

modified theorem euclidean_domain.dvd_lcm_left

modified theorem euclidean_domain.dvd_lcm_right

modified theorem euclidean_domain.dvd_mod_iff

modified theorem euclidean_domain.eq_div_of_mul_eq_left

modified theorem euclidean_domain.eq_div_of_mul_eq_right

modified theorem euclidean_domain.gcd.induction

modified def euclidean_domain.gcd

modified def euclidean_domain.gcd_a

modified def euclidean_domain.gcd_b

modified theorem euclidean_domain.gcd_dvd

modified theorem euclidean_domain.gcd_dvd_left

modified theorem euclidean_domain.gcd_dvd_right

modified theorem euclidean_domain.gcd_eq_gcd_ab

modified theorem euclidean_domain.gcd_eq_left

modified theorem euclidean_domain.gcd_mul_lcm

modified theorem euclidean_domain.gcd_one_left

modified theorem euclidean_domain.gcd_self

modified theorem euclidean_domain.gcd_val

modified theorem euclidean_domain.gcd_zero_left

modified theorem euclidean_domain.gcd_zero_right

modified def euclidean_domain.lcm

modified theorem euclidean_domain.lcm_dvd

modified theorem euclidean_domain.lcm_dvd_iff

modified theorem euclidean_domain.lcm_eq_zero_iff

modified theorem euclidean_domain.lcm_zero_left

modified theorem euclidean_domain.lcm_zero_right

modified theorem euclidean_domain.lt_one

modified theorem euclidean_domain.mod_eq_sub_mul_div

modified theorem euclidean_domain.mod_eq_zero

modified theorem euclidean_domain.mod_lt

modified theorem euclidean_domain.mod_one

modified theorem euclidean_domain.mod_self

modified theorem euclidean_domain.mod_zero

modified theorem euclidean_domain.mul_div_assoc

modified theorem euclidean_domain.mul_div_cancel

modified theorem euclidean_domain.mul_div_cancel_left

modified theorem euclidean_domain.mul_right_not_lt

modified theorem euclidean_domain.val_dvd_le

modified def euclidean_domain.xgcd

modified def euclidean_domain.xgcd_aux

modified theorem euclidean_domain.xgcd_aux_P

modified theorem euclidean_domain.xgcd_aux_fst

modified theorem euclidean_domain.xgcd_aux_rec

modified theorem euclidean_domain.xgcd_aux_val

modified theorem euclidean_domain.xgcd_val

modified theorem euclidean_domain.xgcd_zero_left

modified theorem euclidean_domain.zero_div

modified theorem euclidean_domain.zero_mod