Commit 2024-10-25 12:58 b5a5319a

View on Github →

chore(Algebra/Associated): split off Prime and Irreducible (#18224) This PR moves definitions about prime and irreducible elements to their own file. I always found it somewhat weird that associated elements and prime elements had to live together. After this PR:

  • Prime, Irreducible and irreducible_iff_prime will live in Algebra/Prime/Defs.lean
  • All results on prime and irreducible elements that do not further need associated elements will live in Algebra/Prime/Lemmas.lean I considered also splitting up Associated/Basic.lean into Defs, Lemmas and Prime, but that might be for a follow-up PR. This is in preparation for further cleaning up Data/Nat/Prime/Defs.lean.

Estimated changes

deleted theorem DvdNotUnit.ne
deleted theorem DvdNotUnit.not_unit
deleted theorem Irreducible.dvd_comm
deleted theorem Irreducible.dvd_symm
deleted theorem Irreducible.map
deleted theorem Irreducible.ne_one
deleted theorem Irreducible.ne_zero
deleted theorem Irreducible.not_dvd_one
deleted theorem Irreducible.not_square
deleted theorem Irreducible.of_map
deleted theorem Irreducible.prime
deleted structure Irreducible
deleted theorem IsSquare.not_irreducible
deleted theorem IsSquare.not_prime
deleted theorem MulEquiv.irreducible_iff
deleted theorem MulEquiv.prime_iff
deleted theorem Prime.dvd_mul
deleted theorem Prime.dvd_of_dvd_pow
deleted theorem Prime.dvd_or_dvd
deleted theorem Prime.dvd_pow_iff_dvd
deleted theorem Prime.isPrimal
deleted theorem Prime.ne_one
deleted theorem Prime.ne_zero
deleted theorem Prime.not_dvd_mul
deleted theorem Prime.not_dvd_one
deleted theorem Prime.not_square
deleted theorem Prime.not_unit
deleted def Prime
deleted theorem comap_prime
deleted theorem irreducible_iff
deleted theorem irreducible_iff_prime
deleted theorem irreducible_isUnit_mul
deleted theorem irreducible_mul_iff
deleted theorem irreducible_mul_isUnit
deleted theorem irreducible_mul_units
deleted theorem irreducible_or_factor
deleted theorem irreducible_units_mul
deleted theorem not_irreducible_one
deleted theorem not_irreducible_pow
deleted theorem not_irreducible_zero
deleted theorem not_prime_one
deleted theorem not_prime_pow
deleted theorem not_prime_zero
deleted theorem of_irreducible_mul
deleted theorem pow_inj_of_not_isUnit
deleted theorem prime_pow_succ_dvd_mul
added theorem Irreducible.dvd_comm
added theorem Irreducible.dvd_symm
added theorem Irreducible.ne_one
added theorem Irreducible.ne_zero
added theorem Irreducible.prime
added structure Irreducible
added theorem Prime.dvd_mul
added theorem Prime.dvd_of_dvd_pow
added theorem Prime.dvd_or_dvd
added theorem Prime.dvd_pow_iff_dvd
added theorem Prime.isPrimal
added theorem Prime.ne_one
added theorem Prime.ne_zero
added theorem Prime.not_dvd_mul
added theorem Prime.not_dvd_one
added theorem Prime.not_unit
added def Prime
added theorem irreducible_iff
added theorem irreducible_iff_prime
added theorem irreducible_or_factor
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 DvdNotUnit.ne
added theorem DvdNotUnit.not_unit
added theorem Irreducible.map
added theorem Irreducible.not_square
added theorem Irreducible.of_map
added theorem IsSquare.not_prime
added theorem MulEquiv.prime_iff
added theorem Prime.not_square
added theorem comap_prime
added theorem irreducible_isUnit_mul
added theorem irreducible_mul_iff
added theorem irreducible_mul_isUnit
added theorem irreducible_mul_units
added theorem irreducible_units_mul
added theorem not_irreducible_pow
added theorem not_prime_pow
added theorem pow_inj_of_not_isUnit
added theorem prime_pow_succ_dvd_mul