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