Commit 2023-01-03 19:16 bfe06a77

View on Github →

feat: port Algebra.GCDMonoid.Basic (#1135)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Associated.lean

added theorem Associates.mk_monoidHom_apply

deleted theorem Associates.mk_monoid_hom_apply

Modified Mathlib/Algebra/Divisibility/Basic.lean

Created Mathlib/Algebra/GCDMonoid/Basic.lean

added theorem Associated.gcd_eq_left

added theorem Associated.gcd_eq_right

added theorem Associates.dvd_out_iff

added theorem Associates.mk_normalize

added theorem Associates.mk_out

added theorem Associates.normalize_out

added theorem Associates.out_dvd_iff

added theorem Associates.out_injective

added theorem Associates.out_mk

added theorem Associates.out_mul

added theorem Associates.out_one

added theorem Associates.out_top

added theorem CommGroupWithZero.coe_normUnit

added theorem CommGroupWithZero.normalize_eq_one

added theorem GCDMonoid.irreducible_iff_prime

added theorem GCDMonoid.prime_of_irreducible

added theorem associated_normalize

added theorem associated_normalize_iff

added def associatesEquivOfUniqueUnits

added theorem dvd_antisymm_of_normalize_eq

added theorem dvd_gcd_iff

added theorem dvd_gcd_mul_of_dvd_mul

added theorem dvd_lcm_left

added theorem dvd_lcm_right

added theorem dvd_mul

added theorem dvd_mul_gcd_of_dvd_mul

added theorem dvd_normalize_iff

added theorem exists_associated_pow_of_mul_eq_pow

added theorem exists_dvd_and_dvd_of_dvd_mul

added theorem exists_eq_pow_of_mul_eq_pow

added theorem extract_gcd

added theorem gcd_assoc'

added theorem gcd_assoc

added theorem gcd_comm'

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_normalize

added theorem gcd_eq_of_dvd_sub_left

added theorem gcd_eq_of_dvd_sub_right

added theorem gcd_eq_right_iff

added theorem gcd_eq_zero_iff

added theorem gcd_greatest

added theorem gcd_greatest_associated

added theorem gcd_mul_dvd_mul_gcd

added theorem gcd_mul_lcm

added theorem gcd_mul_left'

added theorem gcd_mul_left

added theorem gcd_mul_right'

added theorem gcd_mul_right

added theorem gcd_one_left'

added theorem gcd_one_left

added theorem gcd_one_right'

added theorem gcd_one_right

added theorem gcd_pow_left_dvd_pow_gcd

added theorem gcd_pow_right_dvd_pow_gcd

added theorem gcd_same

added theorem gcd_zero_left'

added theorem gcd_zero_left

added theorem gcd_zero_right'

added theorem gcd_zero_right

added theorem isUnit_gcd_of_eq_mul_gcd

added theorem lcm_assoc'

added theorem lcm_assoc

added theorem lcm_comm'

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_normalize

added theorem lcm_eq_of_associated_left

added theorem lcm_eq_of_associated_right

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 normUnit_eq_one

added theorem normUnit_mul_normUnit

added theorem normUnit_one

added def normalizationMonoidOfMonoidHomRightInverse

added def normalize

added theorem normalize_apply

added theorem normalize_associated

added theorem normalize_associated_iff

added theorem normalize_coe_units

added theorem normalize_dvd_iff

added theorem normalize_eq

added theorem normalize_eq_normalize

added theorem normalize_eq_normalize_iff

added theorem normalize_eq_one

added theorem normalize_eq_zero

added theorem normalize_gcd

added theorem normalize_idem

added theorem normalize_lcm

added theorem normalize_one

added theorem normalize_zero

added theorem pow_dvd_of_mul_eq_pow

Modified Mathlib/Data/Nat/Prime.lean

Modified Mathlib/Tactic/SplitIfs.lean