Commit 2023-10-05 18:27 63e33342

View on Github →

chore: Use IsCoprime for ideals. (#7523) Make IsCoprime I J the preferred way to say that two ideals are coprime, provide lemmas translating to other formulations.

Estimated changes

Modified Mathlib/Data/List/TFAE.lean

added theorem List.tfae_cons_self

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

modified theorem Ideal.inf_eq_mul_of_coprime

Modified Mathlib/RingTheory/Ideal/Norm.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

added theorem Ideal.add_eq_one_iff

added theorem Ideal.isCoprime_iff_exists

added theorem Ideal.isCoprime_iff_sup_eq

added theorem Ideal.isCoprime_tfae

added theorem IsCoprime.add_eq

added theorem IsCoprime.codisjoint

added theorem IsCoprime.exists

added theorem IsCoprime.sup_eq