Documentation Verification Report

EuclideanDomain

📁 Source: Mathlib/RingTheory/EuclideanDomain.lean

Statistics

Metric	Count
Definitions `EuclideanDomain`, `gcdMonoid`	2
Theorems `dvd_or_coprime`, `gcd_isUnit_iff`, `isCoprime_of_dvd`, `span_gcd`, `isCoprime_div_gcd_div_gcd`, `isCoprime_div_gcd_div_gcd_of_gcd_ne_zero`, `left_div_gcd_ne_zero`, `right_div_gcd_ne_zero`	8
Total	10

EuclideanDomain

Definitions

Name	Category	Theorems
`gcdMonoid` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_or_coprime` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `toCommRing`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `IsCoprime`	—	`dvd_or_isCoprime` `IsBezout.of_isPrincipalIdealRing` `to_principal_ideal_domain`
`gcd_isUnit_iff` 📖	mathematical	—	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `toCommRing` `gcd` `IsCoprime`	—	`gcd_isUnit_iff` `IsBezout.of_isPrincipalIdealRing` `to_principal_ideal_domain` `instIsDomain`
`isCoprime_of_dvd` 📖	mathematical	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toCommRing` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring`	`IsCoprime` `CommRing.toCommSemiring`	—	`isCoprime_of_dvd` `IsBezout.of_isPrincipalIdealRing` `to_principal_ideal_domain`
`span_gcd` 📖	mathematical	—	`Ideal.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `toCommRing` `Set` `Set.instSingletonSet` `gcd` `Set.instInsert`	—	`span_gcd` `IsBezout.of_isPrincipalIdealRing` `to_principal_ideal_domain` `instIsDomain`

(root)

Definitions

Name	Category	Theorems
`EuclideanDomain` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoprime_div_gcd_div_gcd` 📖	mathematical	—	`IsCoprime` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `EuclideanDomain.instDiv` `GCDMonoid.gcd` `CommSemiring.toCommMonoidWithZero`	—	`gcd_isUnit_iff` `IsBezout.of_isPrincipalIdealRing` `EuclideanDomain.to_principal_ideal_domain` `EuclideanDomain.instIsDomain` `isUnit_gcd_of_eq_mul_gcd` `EuclideanDomain.mul_div_cancel'` `gcd_ne_zero_of_right` `GCDMonoid.gcd_dvd_left` `GCDMonoid.gcd_dvd_right`
`isCoprime_div_gcd_div_gcd_of_gcd_ne_zero` 📖	mathematical	—	`IsCoprime` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `EuclideanDomain.instDiv` `GCDMonoid.gcd` `CommSemiring.toCommMonoidWithZero`	—	`gcd_isUnit_iff` `IsBezout.of_isPrincipalIdealRing` `EuclideanDomain.to_principal_ideal_domain` `EuclideanDomain.instIsDomain` `isUnit_gcd_of_eq_mul_gcd` `EuclideanDomain.mul_div_cancel'` `GCDMonoid.gcd_dvd_left` `GCDMonoid.gcd_dvd_right`
`left_div_gcd_ne_zero` 📖	—	—	—	—	`GCDMonoid.gcd_dvd_left` `mul_ne_zero_iff` `IsDomain.to_noZeroDivisors` `EuclideanDomain.instIsDomain` `mul_comm` `mul_div_cancel_right₀` `EuclideanDomain.toMulDivCancelClass`
`right_div_gcd_ne_zero` 📖	—	—	—	—	`GCDMonoid.gcd_dvd_right` `mul_ne_zero_iff` `IsDomain.to_noZeroDivisors` `EuclideanDomain.instIsDomain` `mul_comm` `mul_div_cancel_right₀` `EuclideanDomain.toMulDivCancelClass`

---

← Back to Index