Documentation Verification Report

Units

📁 Source: Mathlib/Algebra/Divisibility/Units.lean

Statistics

Metric	Count
Definitions `IsRelPrime`	1
Theorems `dvd_of_dvd_mul_left`, `dvd_of_dvd_mul_left_of_isPrimal`, `dvd_of_dvd_mul_right`, `dvd_of_dvd_mul_right_of_isPrimal`, `isUnit_of_dvd`, `mul_dvd`, `mul_dvd_of_left_isPrimal`, `mul_dvd_of_right_isPrimal`, `mul_left`, `mul_left_iff`, `mul_right`, `mul_right_iff`, `of_dvd_left`, `of_dvd_right`, `of_mul_left_left`, `of_mul_left_right`, `of_mul_right_left`, `of_mul_right_right`, `dvd`, `dvd_mul_left`, `dvd_mul_right`, `isPrimal`, `isRelPrime_left`, `isRelPrime_right`, `mul_left_dvd`, `mul_right_dvd`, `coe_dvd`, `dvd_mul_left`, `dvd_mul_right`, `mul_left_dvd`, `mul_right_dvd`, `dvd_pow_self_iff`, `isRelPrime_comm`, `isRelPrime_mul_unit_left`, `isRelPrime_mul_unit_left_left`, `isRelPrime_mul_unit_left_right`, `isRelPrime_mul_unit_right`, `isRelPrime_mul_unit_right_left`, `isRelPrime_mul_unit_right_right`, `isRelPrime_one_left`, `isRelPrime_one_right`, `isRelPrime_self`, `isUnit_iff_dvd_one`, `isUnit_iff_forall_dvd`, `isUnit_of_dvd_one`, `isUnit_of_dvd_unit`, `not_isUnit_of_not_isUnit_dvd`, `symmetric_isRelPrime`	48
Total	49

IsRelPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_of_dvd_mul_left` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid` `semigroupDvd` `Monoid.toSemigroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid`	—	`dvd_of_dvd_mul_right` `mul_comm`
`dvd_of_dvd_mul_left_of_isPrimal` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid` `semigroupDvd` `Monoid.toSemigroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `IsPrimal`	`semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid`	—	`dvd_of_dvd_mul_right_of_isPrimal` `mul_comm`
`dvd_of_dvd_mul_right` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid` `semigroupDvd` `Monoid.toSemigroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid`	—	`dvd_of_dvd_mul_right_of_isPrimal` `DecompositionMonoid.primal`
`dvd_of_dvd_mul_right_of_isPrimal` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid` `semigroupDvd` `Monoid.toSemigroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `IsPrimal`	`semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid`	—	`IsUnit.mul_right_dvd` `isUnit_of_dvd` `of_mul_left_right`
`isUnit_of_dvd` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid` `semigroupDvd` `Monoid.toSemigroup`	`IsUnit` `CommMonoid.toMonoid`	—	`dvd_rfl`
`mul_dvd` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid` `semigroupDvd` `Monoid.toSemigroup`	`semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`mul_dvd_of_left_isPrimal` `DecompositionMonoid.primal`
`mul_dvd_of_left_isPrimal` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid` `semigroupDvd` `Monoid.toSemigroup` `IsPrimal`	`semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`mul_comm` `mul_dvd_of_right_isPrimal` `symm`
`mul_dvd_of_right_isPrimal` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid` `semigroupDvd` `Monoid.toSemigroup` `IsPrimal`	`semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`mul_dvd_mul_left` `dvd_of_dvd_mul_left_of_isPrimal` `symm`
`mul_left` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid`	`IsRelPrime` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`exists_dvd_and_dvd_of_dvd_mul` `IsUnit.mul` `Dvd.dvd.trans` `dvd_mul_right` `dvd_mul_left`
`mul_left_iff` 📖	mathematical	—	`IsRelPrime` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`of_mul_left_left` `of_mul_left_right` `mul_left`
`mul_right` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid`	`IsRelPrime` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`isRelPrime_comm` `mul_left`
`mul_right_iff` 📖	mathematical	—	`IsRelPrime` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`of_mul_right_left` `of_mul_right_right` `mul_right`
`of_dvd_left` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid` `semigroupDvd` `Monoid.toSemigroup`	`IsRelPrime` `CommMonoid.toMonoid`	—	`of_mul_left_left`
`of_dvd_right` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid` `semigroupDvd` `Monoid.toSemigroup`	`IsRelPrime` `CommMonoid.toMonoid`	—	`symm` `of_dvd_left`
`of_mul_left_left` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`IsRelPrime` `CommMonoid.toMonoid`	—	`dvd_mul_of_dvd_left`
`of_mul_left_right` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`IsRelPrime` `CommMonoid.toMonoid`	—	`of_mul_left_left` `mul_comm`
`of_mul_right_left` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`IsRelPrime` `CommMonoid.toMonoid`	—	`isRelPrime_comm` `of_mul_left_left`
`of_mul_right_right` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`IsRelPrime` `CommMonoid.toMonoid`	—	`of_mul_right_left` `mul_comm`

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd` 📖	mathematical	`IsUnit`	`semigroupDvd` `Monoid.toSemigroup`	—	`Units.coe_dvd`
`dvd_mul_left` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid`	`semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`Units.dvd_mul_left`
`dvd_mul_right` 📖	mathematical	`IsUnit`	`semigroupDvd` `Monoid.toSemigroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`Units.dvd_mul_right`
`isPrimal` 📖	mathematical	`IsUnit`	`IsPrimal` `Monoid.toSemigroup`	—	`dvd` `one_dvd` `mul_one`
`isRelPrime_left` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid`	`IsRelPrime` `CommMonoid.toMonoid`	—	`isUnit_of_dvd_unit`
`isRelPrime_right` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid`	`IsRelPrime` `CommMonoid.toMonoid`	—	`IsRelPrime.symm` `isRelPrime_left`
`mul_left_dvd` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid`	`semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`Units.mul_left_dvd`
`mul_right_dvd` 📖	mathematical	`IsUnit`	`semigroupDvd` `Monoid.toSemigroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`Units.mul_right_dvd`

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_dvd` 📖	mathematical	—	`semigroupDvd` `Monoid.toSemigroup` `val`	—	`mul_inv_cancel_left`
`dvd_mul_left` 📖	mathematical	—	`semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `val`	—	`mul_comm` `dvd_mul_right`
`dvd_mul_right` 📖	mathematical	—	`semigroupDvd` `Monoid.toSemigroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `val`	—	`mul_assoc` `mul_inv_cancel_right` `Dvd.dvd.mul_right` `dvd_mul_right`
`mul_left_dvd` 📖	mathematical	—	`semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `val`	—	`mul_comm` `mul_right_dvd`
`mul_right_dvd` 📖	mathematical	—	`semigroupDvd` `Monoid.toSemigroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `val`	—	`mul_assoc` `dvd_trans` `Dvd.intro` `mul_inv` `mul_one`

(root)

Definitions

Name	Category	Theorems
`IsRelPrime` 📖	MathDef	89 math math: `isRelPrime_mul_unit_left_left`, `IsRelPrime.pow_left`, `isRelPrime_self`, `UniqueFactorizationMonoid.exists_reduced_factors`, `IsUnit.isRelPrime_right`, `WfDvdMonoid.isRelPrime_of_no_irreducible_factors`, `IsRelPrime.of_mul_right_right`, `IsRelPrime.neg_left`, `IsRelPrime.add_mul_left_right`, `IsRelPrime.add_mul_left_left`, `IsFractionRing.exists_reduced_fraction`, `Irreducible.isRelPrime_iff_not_dvd`, `IsRelPrime.pow_right_iff`, `IsRelPrime.of_mul_add_right_left`, `IsRelPrime.mul_add_right_left`, `IsRelPrime.neg_neg`, `isRelPrime_mul_unit_right`, `UniqueFactorizationMonoid.prime_pow_coprime_prod_of_coprime_insert`, `IsRelPrime.neg_right`, `IsRelPrime.mul_add_left_right`, `IsRelPrime.mul_left`, `isRelPrime_zero_right`, `IsRelPrime.mul_add_left_left`, `isRelPrime_one_right`, `IsRelPrime.of_mul_add_right_right`, `IsRelPrime.neg_left_iff`, `IsRelPrime.symm`, `IsRelPrime.mul_add_right_right`, `not_isRelPrime_zero_zero`, `IsRelPrime.pow_iff`, `IsRelPrime.add_mul_right_right`, `IsRelPrime.prod_left`, `IsRelPrime.of_add_mul_left_right`, `IsRelPrime.of_mul_left_left`, `IsRelPrime.add_mul_right_left_iff`, `IsRelPrime.add_mul_left_left_iff`, `IsRelPrime.prod_right`, `IsRelPrime.of_add_mul_right_right`, `IsRelPrime.of_mul_right_left`, `isRelPrime_mul_unit_right_left`, `IsRelPrime.pow_left_iff`, `IsRelPrime.of_add_mul_left_left`, `IsUnit.isRelPrime_left`, `IsRelPrime.pow_right`, `isRelPrime_of_no_nonunits_factors`, `IsRelPrime.neg_right_iff`, `IsRelPrime.mul_add_left_left_iff`, `squarefree_mul_iff`, `IsRelPrime.mul_add_right_left_iff`, `IsRelPrime.of_add_mul_right_left`, `IsRelPrime.of_mul_add_left_left`, `isRelPrime_comm`, `IsRelPrime.add_mul_left_right_iff`, `IsRelPrime.add_mul_right_left`, `UniqueFactorizationMonoid.pairwise_primeFactors_isRelPrime`, `isRelPrime_mul_unit_right_right`, `isRelPrime_mul_unit_left_right`, `IsRelPrime.mul_left_iff`, `gcd_isUnit_iff_isRelPrime`, `IsRelPrime.pow`, `IsRelPrime.of_dvd_right`, `IsRelPrime.prod_left_iff`, `IsCoprime.isRelPrime`, `isRelPrime_iff_isCoprime`, `isRelPrime_mul_unit_left`, `Irreducible.dvd_or_isRelPrime`, `IsRelPrime.of_prod_right`, `Associates.mk_isRelPrime_iff`, `IsRelPrime.of_prod_left`, `IsRelPrime.mul_add_left_right_iff`, `IsRelPrime.of_dvd_left`, `IsRelPrime.mul_add_right_right_iff`, `pairwise_isRelPrime_iff_isRelPrime_prod`, `IsFractionRing.num_den_reduced`, `IsRelPrime.of_map`, `isRelPrime_one_left`, `UniqueFactorizationMonoid.isRelPrime_iff_no_prime_factors`, `isRelPrime_zero_left`, `IsRelPrime.neg_neg_iff`, `IsRelPrime.prod_right_iff`, `IsRelPrime.of_squarefree_mul`, `IsRelPrime.add_mul_right_right_iff`, `IsRelPrime.mul_right`, `IsRelPrime.of_mul_add_left_right`, `symmetric_isRelPrime`, `UniqueFactorizationMonoid.exists_reduced_factors'`, `Nat.coprime_iff_isRelPrime`, `IsRelPrime.of_mul_left_right`, `IsRelPrime.mul_right_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_pow_self_iff` 📖	mathematical	—	`semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `Monoid.toPow` `IsUnit`	—	`eq_or_ne` `pow_zero`
`isRelPrime_comm` 📖	mathematical	—	`IsRelPrime` `CommMonoid.toMonoid`	—	`IsRelPrime.symm`
`isRelPrime_mul_unit_left` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid`	`IsRelPrime` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`isRelPrime_mul_unit_left_left` `isRelPrime_mul_unit_left_right`
`isRelPrime_mul_unit_left_left` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid`	`IsRelPrime` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`IsRelPrime.of_mul_left_right` `IsUnit.dvd_mul_left`
`isRelPrime_mul_unit_left_right` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid`	`IsRelPrime` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`isRelPrime_comm` `isRelPrime_mul_unit_left_left`
`isRelPrime_mul_unit_right` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid`	`IsRelPrime` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`isRelPrime_mul_unit_right_left` `isRelPrime_mul_unit_right_right`
`isRelPrime_mul_unit_right_left` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid`	`IsRelPrime` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`mul_comm` `isRelPrime_mul_unit_left_left`
`isRelPrime_mul_unit_right_right` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid`	`IsRelPrime` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`mul_comm` `isRelPrime_mul_unit_left_right`
`isRelPrime_one_left` 📖	mathematical	—	`IsRelPrime` `CommMonoid.toMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`IsUnit.isRelPrime_left` `isUnit_one`
`isRelPrime_one_right` 📖	mathematical	—	`IsRelPrime` `CommMonoid.toMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`IsUnit.isRelPrime_right` `isUnit_one`
`isRelPrime_self` 📖	mathematical	—	`IsRelPrime` `CommMonoid.toMonoid` `IsUnit`	—	`dvd_rfl` `isUnit_of_dvd_unit`
`isUnit_iff_dvd_one` 📖	mathematical	—	`IsUnit` `CommMonoid.toMonoid` `semigroupDvd` `Monoid.toSemigroup` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`IsUnit.dvd` `mul_comm`
`isUnit_iff_forall_dvd` 📖	mathematical	—	`IsUnit` `CommMonoid.toMonoid` `semigroupDvd` `Monoid.toSemigroup`	—	`isUnit_iff_dvd_one` `Dvd.dvd.trans` `one_dvd`
`isUnit_of_dvd_one` 📖	mathematical	`semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`IsUnit` `CommMonoid.toMonoid`	—	`isUnit_iff_dvd_one`
`isUnit_of_dvd_unit` 📖	mathematical	`semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `IsUnit`	`IsUnit` `CommMonoid.toMonoid`	—	`isUnit_iff_dvd_one` `Dvd.dvd.trans`
`not_isUnit_of_not_isUnit_dvd` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid` `semigroupDvd` `Monoid.toSemigroup`	`IsUnit` `CommMonoid.toMonoid`	—	`isUnit_of_dvd_unit`
`symmetric_isRelPrime` 📖	mathematical	—	`Symmetric` `IsRelPrime` `CommMonoid.toMonoid`	—	`IsRelPrime.symm`

---

← Back to Index