Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-31 17:48 20b41439

View on Github →

feat(algebra): add normalization and GCD domain; setup for int

Estimated changes

Created algebra/gcd_domain.lean

added theorem associated_of_dvd_of_dvd

added theorem dvd_antisymm_of_norm

added theorem dvd_gcd_iff

added theorem dvd_lcm_left

added theorem dvd_lcm_right

added theorem gcd_assoc

added theorem gcd_comm

added theorem gcd_dvd_gcd

added theorem gcd_dvd_gcd_mul_left

added theorem gcd_dvd_gcd_mul_left_right

added theorem gcd_dvd_gcd_mul_right

added theorem gcd_dvd_gcd_mul_right_right

added theorem gcd_eq_left_iff

added theorem gcd_eq_mul_norm_unit

added theorem gcd_eq_right_iff

added theorem gcd_eq_zero_iff

added theorem gcd_mul_lcm

added theorem gcd_mul_left

added theorem gcd_mul_right

added theorem gcd_one_left

added theorem gcd_one_right

added theorem gcd_same

added theorem gcd_zero_left

added theorem gcd_zero_right

added theorem lcm_assoc

added theorem lcm_comm

added theorem lcm_dvd

added theorem lcm_dvd_iff

added theorem lcm_dvd_lcm

added theorem lcm_dvd_lcm_mul_left

added theorem lcm_dvd_lcm_mul_left_right

added theorem lcm_dvd_lcm_mul_right

added theorem lcm_dvd_lcm_mul_right_right

added theorem lcm_eq_left_iff

added theorem lcm_eq_mul_norm_unit

added theorem lcm_eq_one_iff

added theorem lcm_eq_right_iff

added theorem lcm_eq_zero_iff

added theorem lcm_mul_left

added theorem lcm_mul_right

added theorem lcm_one_left

added theorem lcm_one_right

added theorem lcm_same

added theorem lcm_units_coe_left

added theorem lcm_units_coe_right

added theorem mul_norm_unit_eq_mul_norm_unit

added theorem norm_unit_gcd

added theorem norm_unit_lcm

added theorem norm_unit_mul_norm_unit

added theorem norm_unit_one

Modified data/int/gcd.lean

added theorem int.coe_gcd

added theorem int.coe_lcm

added theorem int.coe_nat_abs_eq_mul_norm_unit

modified theorem int.dvd_gcd

deleted theorem int.eq_zero_of_gcd_eq_zero_left

deleted theorem int.eq_zero_of_gcd_eq_zero_right

modified theorem int.gcd_assoc

modified theorem int.gcd_comm

deleted theorem int.gcd_dvd

added theorem int.gcd_eq_zero_iff

modified theorem int.gcd_one_right

modified theorem int.gcd_self

modified theorem int.gcd_zero_right

modified def int.lcm

modified theorem int.lcm_def

modified theorem int.lcm_dvd

modified theorem int.lcm_one_left

modified theorem int.lcm_one_right

modified theorem int.lcm_self

modified theorem int.lcm_zero_left

modified theorem int.lcm_zero_right

added theorem int.nat_abs_gcd

added theorem int.nat_abs_lcm

added theorem int.norm_unit_nat_coe

added theorem int.norm_unit_of_neg

added theorem int.norm_unit_of_nonneg