Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2018-09-02 20:50
dd0c0aee
View on Github →
feat(ring_theory): add unique factorization domain
Estimated changes
Created
ring_theory/unique_factorization_domain.lean
added
theorem
associates.eq_of_factors_eq_factors
added
theorem
associates.eq_of_prod_eq_prod
added
theorem
associates.factor_set.coe_add
added
def
associates.factor_set.prod
added
theorem
associates.factor_set.sup_add_inf_eq_add
added
def
associates.factors'
added
theorem
associates.factors'_cong
added
def
associates.factors
added
theorem
associates.factors_0
added
theorem
associates.factors_le
added
theorem
associates.factors_mk
added
theorem
associates.factors_mono
added
theorem
associates.factors_mul
added
theorem
associates.factors_prod
added
theorem
associates.map_subtype_val_factors'
added
theorem
associates.prod_add
added
theorem
associates.prod_coe
added
theorem
associates.prod_factors
added
theorem
associates.prod_le
added
theorem
associates.prod_le_prod_iff_le
added
theorem
associates.prod_mono
added
theorem
associates.prod_top
added
theorem
associates.sup_mul_inf
added
theorem
associates.unique'
added
def
associates.{u}
added
def
unique_factorization_domain.to_gcd_domain