Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-16 04:45 2c930a37

View on Github →

refactor(algebra/gcd_monoid, ring_theory/multiplicity): generalize normalization_domain, gcd_domain, multiplicity (#3779)

  • generalize normalization_domain, gcd_domain, multiplicity to not reference addition and subtraction
  • make gcd_monoid and normalization_monoid into mixins
  • add instances of normalization_monoid for nat, associates

Estimated changes

modified theorem associates.coe_unit_eq_one
modified theorem dvd_normalize_iff
modified theorem int.coe_gcd
modified theorem int.coe_lcm
modified theorem int.nat_abs_gcd
modified theorem int.nat_abs_lcm
added theorem norm_unit_eq_one
modified theorem norm_unit_mul_norm_unit
modified def normalize
added theorem normalize_apply
modified theorem normalize_coe_units
modified theorem normalize_dvd_iff
added theorem normalize_eq
modified theorem normalize_idem
deleted theorem normalize_mul
modified theorem normalize_one
modified theorem normalize_zero
added theorem units_eq_one
modified theorem polynomial.degree_normalize
modified def multiplicity