Commit 2023-10-04 12:39 1b346a7b

View on Github →

feat: add some ring theory lemmas (#7466) From flt-regular.

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

added theorem Ideal.isCoprime_iff_gcd

Modified Mathlib/RingTheory/Ideal/Norm.lean

added theorem Ideal.absNorm_eq_zero_iff

added theorem Ideal.norm_dvd_iff

added theorem Ideal.span_singleton_absNorm

Modified Mathlib/RingTheory/Ideal/Operations.lean

added theorem Ideal.isCoprime_iff_add

added theorem Ideal.isCoprime_iff_codisjoint

added theorem Ideal.isCoprime_span_singleton_iff

Modified Mathlib/RingTheory/Ideal/Quotient.lean

added theorem Ideal.Quotient.eq_zero_iff_dvd

Modified Mathlib/RingTheory/RootsOfUnity/Basic.lean

added theorem IsPrimitiveRoot.sub_one_ne_zero

Modified Mathlib/RingTheory/Subsemiring/Basic.lean