Commit 2025-01-23 12:20 da8db712

View on Github →

chore: fix some declarations using coprime (#20982) Overwhelmingly isCoprime is used in names when it is also used in the theorem statement. Here we fix the last instances where coprime was used instead. Follow up to #20976.

Estimated changes

Modified Mathlib/FieldTheory/SeparableDegree.lean

Modified Mathlib/NumberTheory/DiophantineApproximation/Basic.lean

Modified Mathlib/NumberTheory/FLT/Four.lean

deleted theorem Int.coprime_of_sq_sum'

deleted theorem Int.coprime_of_sq_sum

added theorem Int.isCoprime_of_sq_sum'

added theorem Int.isCoprime_of_sq_sum

Modified Mathlib/NumberTheory/Zsqrtd/Basic.lean

deleted theorem Zsqrtd.coprime_of_dvd_coprime

added theorem Zsqrtd.isCoprime_of_dvd_isCoprime

Modified Mathlib/RingTheory/EuclideanDomain.lean

Modified Mathlib/RingTheory/Int/Basic.lean

deleted theorem Int.coprime_iff_nat_coprime

added theorem Int.isCoprime_iff_nat_coprime

deleted theorem Int.sq_of_coprime

added theorem Int.sq_of_isCoprime

Modified Mathlib/RingTheory/Polynomial/Basic.lean

deleted theorem Polynomial.disjoint_ker_aeval_of_coprime

added theorem Polynomial.disjoint_ker_aeval_of_isCoprime

deleted theorem Polynomial.sup_aeval_range_eq_top_of_coprime

added theorem Polynomial.sup_aeval_range_eq_top_of_isCoprime

Modified Mathlib/RingTheory/PrincipalIdealDomain.lean

deleted theorem Irreducible.coprime_or_dvd

deleted theorem Irreducible.dvd_iff_not_coprime

added theorem Irreducible.dvd_iff_not_isCoprime

added theorem Irreducible.isCoprime_or_dvd

deleted theorem dvd_or_coprime

added theorem dvd_or_isCoprime

Modified Mathlib/RingTheory/RootsOfUnity/Minpoly.lean