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