Coprime

📁 Source: Mathlib/Data/ZMod/Coprime.lean

Statistics

Metric	Count
Definitions Coprime	1
Theorems coe_int_isUnit_iff_isCoprime, eq_zero_iff_gcd_ne_one, eq_zero_of_gcd_ne_one, ne_zero_of_gcd_eq_one	4
Total	5

PNat

Definitions

Name	Category	Theorems
Coprime 📖	MathDef	3 math math: coprime_coe, one_coprime, coprime_one

ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_int_isUnit_iff_isCoprime 📖	mathematical	—	IsUnit ZMod MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring commRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing IsCoprime Int.instCommSemiring	—	Int.isCoprime_iff_nat_coprime isUnit_iff_coprime Associated.isUnit_iff eq_intCast RingHom.instRingHomClass Int.cast_natCast Associated.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Int.associated_natAbs
eq_zero_iff_gcd_ne_one 📖	mathematical	—	ZMod AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing commRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Int.isCoprime_iff_gcd_eq_one Prime.coprime_iff_not_dvd IsBezout.of_isPrincipalIdealRing EuclideanDomain.to_principal_ideal_domain Int.instIsDomain Nat.prime_iff_prime_int Fact.out intCast_zmod_eq_zero_iff_dvd
eq_zero_of_gcd_ne_one 📖	mathematical	Nat.Prime	ZMod AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing commRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	eq_zero_iff_gcd_ne_one
ne_zero_of_gcd_eq_one 📖	—	Nat.Prime	—	—	eq_zero_iff_gcd_ne_one

---

← Back to Index