Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2018-09-02 20:50
5f8fafcf
View on Github →
feat(ring_theory): add associated elements
Estimated changes
Modified
algebra/ring.lean
modified
theorem
mul_eq_zero
added
theorem
zero_eq_mul
Modified
data/multiset.lean
added
theorem
multiset.exists_multiset_eq_map_quot_mk
added
theorem
multiset.induction_on_multiset_quot
added
theorem
multiset.injective_map
added
theorem
multiset.map_eq_map
added
theorem
multiset.map_mk_eq_map_mk_of_rel
Modified
data/nat/basic.lean
Modified
order/bounded_lattice.lean
added
theorem
with_top.coe_inf
added
theorem
with_top.coe_sup
Created
ring_theory/associated_elements.lean
added
theorem
associated.associated_of_dvd_dvd
added
theorem
associated.associated_one_iff_is_unit
added
theorem
associated.associated_one_of_associated_mul_one
added
theorem
associated.associated_one_of_mul_eq_one
added
theorem
associated.associated_zero_iff_eq_zero
added
theorem
associated.unit_associated_one
added
def
associated
added
theorem
associates.coe_unit_eq_one
added
theorem
associates.dvd_of_mk_le_mk
added
theorem
associates.dvd_out_iff
added
theorem
associates.forall_associated
added
theorem
associates.irreducible_mk_iff
added
theorem
associates.is_unit_iff_eq_one
added
theorem
associates.is_unit_mk
added
theorem
associates.le_mul_left
added
theorem
associates.le_mul_right
added
theorem
associates.mk_eq_mk_iff_associated
added
theorem
associates.mk_eq_zero_iff_eq_zero
added
theorem
associates.mk_le_mk_iff_dvd_iff
added
theorem
associates.mk_le_mk_of_dvd
added
theorem
associates.mk_mul_mk
added
theorem
associates.mk_zero_eq
added
theorem
associates.mul_eq_one_iff
added
theorem
associates.mul_eq_zero_iff
added
theorem
associates.mul_mono
added
theorem
associates.mul_zero
added
theorem
associates.norm_unit_out
added
theorem
associates.one_eq_mk_one
added
theorem
associates.one_le
added
theorem
associates.out_dvd_iff
added
theorem
associates.out_mk
added
theorem
associates.out_mul
added
theorem
associates.out_one
added
theorem
associates.out_top
added
theorem
associates.prod_eq_one_iff
added
theorem
associates.prod_eq_zero_iff
added
theorem
associates.prod_le_prod
added
theorem
associates.prod_mk
added
theorem
associates.quot_mk_eq_mk
added
theorem
associates.quotient_mk_eq_mk
added
theorem
associates.rel_associated_iff_map_eq_map
added
theorem
associates.zero_mul
added
theorem
associates.zero_ne_one
added
def
associates
added
def
associates_int_equiv_nat
added
def
irreducible
added
theorem
irreducible_iff_nat_prime
added
def
is_unit
added
theorem
is_unit_mul_units
added
theorem
is_unit_nat
added
theorem
is_unit_one
added
theorem
not_irreducible_one
added
theorem
not_irreducible_zero
added
theorem
not_is_unit_zero
added
theorem
units.is_unit_of_mul_one
Modified
ring_theory/localization.lean