Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-10 21:50 091cad78

View on Github →

feat(algebra/gcd_domain): normalize (#668)

Estimated changes

Modified src/algebra/gcd_domain.lean

added theorem associated_normalize

deleted theorem associated_of_dvd_of_dvd

deleted theorem associates.norm_unit_out

added theorem associates.normalize_out

modified theorem associates.out_mk

deleted theorem dvd_antisymm_of_norm

added theorem dvd_antisymm_of_normalize_eq

added theorem dvd_normalize_iff

modified theorem gcd_eq_left_iff

deleted theorem gcd_eq_mul_norm_unit

added theorem gcd_eq_normalize

modified theorem gcd_eq_right_iff

modified theorem gcd_mul_lcm

modified theorem gcd_mul_left

modified theorem gcd_mul_right

modified theorem gcd_same

modified theorem gcd_zero_left

modified theorem gcd_zero_right

deleted theorem int.coe_nat_abs_eq_mul_norm_unit

added theorem int.coe_nat_abs_eq_normalize

deleted theorem int.norm_unit_nat_coe

deleted theorem int.norm_unit_of_neg

deleted theorem int.norm_unit_of_nonneg

added theorem int.normalize_coe_nat

added theorem int.normalize_of_neg

added theorem int.normalize_of_nonneg

modified theorem lcm_eq_left_iff

deleted theorem lcm_eq_mul_norm_unit

added theorem lcm_eq_normalize

modified theorem lcm_eq_right_iff

modified theorem lcm_mul_left

modified theorem lcm_mul_right

modified theorem lcm_one_left

modified theorem lcm_one_right

modified theorem lcm_same

modified theorem lcm_units_coe_left

modified theorem lcm_units_coe_right

deleted theorem mul_norm_unit_eq_mul_norm_unit

deleted theorem norm_unit_gcd

deleted theorem norm_unit_lcm

added def normalize

added theorem normalize_associated

added theorem normalize_coe_units

added theorem normalize_dvd_iff

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_mul

added theorem normalize_one

added theorem normalize_zero

Modified src/data/polynomial.lean

deleted theorem polynomial.monic_mul_norm_unit

added theorem polynomial.monic_normalize

Modified src/ring_theory/unique_factorization_domain.lean