Commit 2024-09-30 02:32 ab337098

View on Github →

chore(Associated): use M, N for type variables (#17115) Replace α → M, β → N for type variables.

Estimated changes

modified theorem Associated.dvd_iff_dvd_left
modified theorem Associated.eq_zero_iff
modified theorem Associated.isUnit_iff
modified theorem Associated.mul_left
modified theorem Associated.mul_mul
modified theorem Associated.mul_right
modified theorem Associated.ne_zero_iff
modified theorem Associated.neg_left
modified theorem Associated.neg_neg
modified theorem Associated.neg_right
modified theorem Associated.of_mul_left
modified theorem Associated.of_mul_right
modified theorem Associated.pow_pow
modified theorem Associated.prime_iff
modified def Associated
modified theorem Associates.Prime.le_or_le
modified theorem Associates.bot_eq_one
modified theorem Associates.coe_unit_eq_one
modified theorem Associates.dvdNotUnit_of_lt
modified theorem Associates.dvd_eq_le
modified theorem Associates.dvd_of_mk_le_mk
modified theorem Associates.exists_rep
modified theorem Associates.irreducible_mk
modified theorem Associates.isPrimal_mk
modified theorem Associates.isUnit_mk
modified theorem Associates.le_mul_left
modified theorem Associates.le_mul_right
modified theorem Associates.le_one_iff
modified theorem Associates.mk_dvd_mk
modified theorem Associates.mk_eq_one
modified theorem Associates.mk_eq_zero
modified theorem Associates.mk_injective
modified theorem Associates.mk_le_mk_iff_dvd
modified theorem Associates.mk_le_mk_of_dvd
modified theorem Associates.mk_mul_mk
modified theorem Associates.mk_ne_zero
modified theorem Associates.mk_one
modified theorem Associates.mk_pow
modified theorem Associates.mk_quot_out
modified theorem Associates.mk_surjective
modified theorem Associates.mk_zero
modified theorem Associates.mul_mono
modified theorem Associates.one_eq_mk_one
modified theorem Associates.one_le
modified theorem Associates.prime_mk
modified theorem Associates.quot_mk_eq_mk
modified theorem Associates.quot_out
modified theorem Associates.quot_out_zero
modified theorem DvdNotUnit.ne
modified theorem DvdNotUnit.not_associated
modified theorem DvdNotUnit.not_unit
modified theorem Irreducible.dvd_comm
modified theorem Irreducible.dvd_iff
modified theorem Irreducible.dvd_symm
modified theorem Irreducible.ne_one
modified theorem Irreducible.ne_zero
modified theorem Irreducible.not_dvd_one
modified theorem Irreducible.prime
modified structure Irreducible
modified theorem MulEquiv.prime_iff
modified theorem Prime.associated_of_dvd
modified theorem Prime.dvd_mul
modified theorem Prime.dvd_of_dvd_pow
modified theorem Prime.dvd_or_dvd
modified theorem Prime.dvd_pow_iff_dvd
modified theorem Prime.not_dvd_mul
modified def Prime
modified theorem associated_eq_eq
modified theorem associated_iff_eq
modified theorem associated_mul_unit_left
modified theorem associated_mul_unit_right
modified theorem associated_of_dvd_dvd
modified theorem associated_one_iff_isUnit
modified theorem associated_unit_mul_left
modified theorem associated_unit_mul_right
modified theorem associated_zero_iff_eq_zero
modified theorem comap_prime
modified theorem dvd_dvd_iff_associated
modified theorem dvd_prime_pow
modified theorem irreducible_iff
modified theorem irreducible_iff_prime
modified theorem irreducible_isUnit_mul
modified theorem irreducible_mul_iff
modified theorem irreducible_mul_isUnit
modified theorem irreducible_mul_units
modified theorem irreducible_or_factor
modified theorem irreducible_units_mul
modified theorem isUnit_of_associated_mul
modified theorem not_irreducible_one
modified theorem not_irreducible_pow
modified theorem not_irreducible_zero
modified theorem not_prime_one
modified theorem not_prime_zero
modified theorem of_irreducible_mul
modified theorem pow_inj_of_not_isUnit
modified theorem pow_injective_of_not_isUnit
modified theorem prime_mul_iff
modified theorem prime_pow_iff
modified theorem prime_pow_succ_dvd_mul
modified theorem unit_associated_one