Commit 2023-10-02 06:27 51089d8f

View on Github →

feat: some lemmas about associated and prime elements (#7453) From flt-regular.

Estimated changes

Modified Mathlib/Algebra/Associated.lean

modified theorem Irreducible.associated_of_dvd

added theorem Irreducible.dvd_iff

modified theorem Irreducible.dvd_irreducible_iff_associated

added theorem Irreducible.isUnit_iff_not_associated_of_dvd

added theorem Prime.dvd_mul

added theorem Prime.not_dvd_mul

Modified Mathlib/Algebra/GCDMonoid/Basic.lean

added theorem Irreducible.gcd_eq_one_iff

added theorem Irreducible.isUnit_gcd_iff

added theorem associated_gcd_left_iff

added theorem associated_gcd_right_iff

added theorem dvd_gcd_mul_iff_dvd_mul

added theorem dvd_mul_gcd_iff_dvd_mul

Modified test/propose.lean