Commit 2022-12-20 05:33 69dfd0b5

View on Github →

feat: port Algebra.Associated (#1098) dcf2250875895376a142faeeac5eabff32c48655

depends on #1055
depends on #1092

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Associated.lean

added theorem Associated.dvd_iff_dvd_left

added theorem Associated.dvd_iff_dvd_right

added theorem Associated.eq_zero_iff

added theorem Associated.isUnit_iff

added theorem Associated.mul_left

added theorem Associated.mul_mul

added theorem Associated.mul_right

added theorem Associated.ne_zero_iff

added theorem Associated.of_mul_left

added theorem Associated.of_mul_right

added theorem Associated.of_pow_associated_of_prime'

added theorem Associated.of_pow_associated_of_prime

added theorem Associated.pow_pow

added theorem Associated.prime_iff

added def Associated

added theorem Associates.Prime.le_or_le

added theorem Associates.associated_map_mk

added theorem Associates.bot_eq_one

added theorem Associates.coe_unit_eq_one

added theorem Associates.dvdNotUnit_iff_lt

added theorem Associates.dvdNotUnit_of_lt

added theorem Associates.dvd_eq_le

added theorem Associates.dvd_of_mk_le_mk

added theorem Associates.eq_of_mul_eq_mul_left

added theorem Associates.eq_of_mul_eq_mul_right

added theorem Associates.exists_non_zero_rep

added theorem Associates.exists_rep

added theorem Associates.forall_associated

added theorem Associates.irreducible_iff_prime_iff

added theorem Associates.irreducible_mk

added theorem Associates.isUnit_iff_eq_bot

added theorem Associates.isUnit_iff_eq_one

added theorem Associates.isUnit_mk

added theorem Associates.le_mul_left

added theorem Associates.le_mul_right

added theorem Associates.le_of_mul_le_mul_left

added theorem Associates.le_one_iff

added theorem Associates.mk_dvdNotUnit_mk_iff

added theorem Associates.mk_dvd_mk

added theorem Associates.mk_eq_mk_iff_associated

added theorem Associates.mk_eq_zero

added theorem Associates.mk_injective

added theorem Associates.mk_le_mk_iff_dvd_iff

added theorem Associates.mk_le_mk_of_dvd

added theorem Associates.mk_monoid_hom_apply

added theorem Associates.mk_mul_mk

added theorem Associates.mk_ne_zero

added theorem Associates.mk_one

added theorem Associates.mk_pow

added theorem Associates.mk_surjective

added theorem Associates.mul_eq_one_iff

added theorem Associates.mul_mono

added theorem Associates.one_eq_mk_one

added theorem Associates.one_le

added theorem Associates.one_or_eq_of_le_of_prime

added theorem Associates.prime_mk

added theorem Associates.quot_mk_eq_mk

added theorem Associates.quotient_mk_eq_mk

added theorem Associates.units_eq_one

added theorem DvdNotUnit.isUnit_of_irreducible_right

added theorem DvdNotUnit.ne

added theorem DvdNotUnit.not_associated

added theorem DvdNotUnit.not_unit

added theorem Irreducible.associated_of_dvd

added theorem Irreducible.dvd_comm

added theorem Irreducible.dvd_irreducible_iff_associated

added theorem Irreducible.dvd_symm

added theorem Irreducible.isUnit_or_isUnit

added theorem Irreducible.ne_one

added theorem Irreducible.ne_zero

added theorem Irreducible.not_dvd_one

added theorem Irreducible.not_square

added structure Irreducible

added theorem IsSquare.not_irreducible

added theorem IsSquare.not_prime

added theorem MulEquiv.prime_iff

added theorem Prime.associated_of_dvd

added theorem Prime.dvd_of_dvd_pow

added theorem Prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd

added theorem Prime.dvd_or_dvd

added theorem Prime.dvd_prime_iff_associated

added theorem Prime.left_dvd_or_dvd_right_of_dvd_mul

added theorem Prime.ne_one

added theorem Prime.ne_zero

added theorem Prime.not_dvd_one

added theorem Prime.not_square

added theorem Prime.not_unit

added theorem Prime.pow_dvd_of_dvd_mul_left

added theorem Prime.pow_dvd_of_dvd_mul_right

added def Prime

added theorem associated_eq_eq

added theorem associated_iff_eq

added theorem associated_isUnit_mul_left_iff

added theorem associated_isUnit_mul_right_iff

added theorem associated_mul_isUnit_left_iff

added theorem associated_mul_isUnit_right_iff

added theorem associated_mul_unit_left

added theorem associated_mul_unit_left_iff

added theorem associated_mul_unit_right

added theorem associated_mul_unit_right_iff

added theorem associated_of_dvd_dvd

added theorem associated_one_iff_isUnit

added theorem associated_one_of_associated_mul_one

added theorem associated_one_of_mul_eq_one

added theorem associated_unit_mul_left

added theorem associated_unit_mul_left_iff

added theorem associated_unit_mul_right

added theorem associated_unit_mul_right_iff

added theorem associated_zero_iff_eq_zero

added theorem comap_prime

added theorem dvdNotUnit_of_dvdNotUnit_associated

added theorem dvd_dvd_iff_associated

added theorem dvd_prime_pow

added theorem eq_of_prime_pow_eq'

added theorem eq_of_prime_pow_eq

added theorem irreducible_iff

added theorem irreducible_isUnit_mul

added theorem irreducible_mul_iff

added theorem irreducible_mul_isUnit

added theorem irreducible_mul_units

added theorem irreducible_or_factor

added theorem irreducible_units_mul

added theorem isUnit_of_associated_mul

added theorem not_irreducible_of_not_unit_dvdNotUnit

added theorem not_irreducible_one

added theorem not_irreducible_zero

added theorem not_prime_one

added theorem not_prime_zero

added theorem of_irreducible_mul

added theorem of_irreducible_pow

added theorem pow_injective_of_not_unit

added theorem pow_not_prime

added theorem prime_dvd_prime_iff_eq

added theorem prime_pow_succ_dvd_mul

added theorem succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul

added theorem unit_associated_one

added theorem units_eq_one