Basic

📁 Source: Mathlib/RingTheory/Coprime/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `abs_abs`, `abs_abs_iff`, `abs_left`, `abs_left_iff`, `abs_right`, `abs_right_iff`, `add_mul_left_left`, `add_mul_left_left_iff`, `add_mul_left_right`, `add_mul_left_right_iff`, `add_mul_right_left`, `add_mul_right_left_iff`, `add_mul_right_right`, `add_mul_right_right_iff`, `dvd_of_dvd_mul_left`, `dvd_of_dvd_mul_right`, `intCast`, `isRelPrime`, `isUnit_of_dvd`, `isUnit_of_dvd'`, `map`, `mono`, `mul_add_left_left`, `mul_add_left_left_iff`, `mul_add_left_right`, `mul_add_left_right_iff`, `mul_add_right_left`, `mul_add_right_left_iff`, `mul_add_right_right`, `mul_add_right_right_iff`, `mul_dvd`, `mul_left`, `mul_left_iff`, `mul_right`, `mul_right_iff`, `ne_zero`, `ne_zero_or_ne_zero`, `neg_left`, `neg_left_iff`, `neg_neg`, `neg_neg_iff`, `neg_right`, `neg_right_iff`, `of_add_mul_left_left`, `of_add_mul_left_right`, `of_add_mul_right_left`, `of_add_mul_right_right`, `of_isCoprime_of_dvd_left`, `of_isCoprime_of_dvd_right`, `of_mul_add_left_left`, `of_mul_add_left_right`, `of_mul_add_right_left`, `of_mul_add_right_right`, `of_mul_left_left`, `of_mul_left_right`, `of_mul_right_left`, `of_mul_right_right`, `sq_add_sq_ne_zero`, `add_mul_left_left`, `add_mul_left_left_iff`, `add_mul_left_right`, `add_mul_left_right_iff`, `add_mul_right_left`, `add_mul_right_left_iff`, `add_mul_right_right`, `add_mul_right_right_iff`, `mul_add_left_left`, `mul_add_left_left_iff`, `mul_add_left_right`, `mul_add_left_right_iff`, `mul_add_right_left`, `mul_add_right_left_iff`, `mul_add_right_right`, `mul_add_right_right_iff`, `neg_left`, `neg_left_iff`, `neg_neg`, `neg_neg_iff`, `neg_right`, `neg_right_iff`, `of_add_mul_left_left`, `of_add_mul_left_right`, `of_add_mul_right_left`, `of_add_mul_right_right`, `of_mul_add_left_left`, `of_mul_add_left_right`, `of_mul_add_right_left`, `of_mul_add_right_right`, `isCoprime_iff`, `isCoprime_iff`, `isCoprime_iff`, `isCoprime_comm`, `isCoprime_group_smul`, `isCoprime_group_smul_left`, `isCoprime_group_smul_right`, `isCoprime_mul_unit_left`, `isCoprime_mul_unit_left_left`, `isCoprime_mul_unit_left_right`, `isCoprime_mul_unit_right`, `isCoprime_mul_unit_right_left`, `isCoprime_mul_unit_right_right`, `isCoprime_mul_units_left`, `isCoprime_mul_units_right`, `isCoprime_one_left`, `isCoprime_one_right`, `isCoprime_self`, `isCoprime_zero_left`, `isCoprime_zero_right`, `not_isCoprime_zero_zero`	109
Total	109

IsCoprime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_abs` 📖	mathematical	`IsCoprime` `CommRing.toCommSemiring`	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`abs_right` `abs_left`
`abs_abs_iff` 📖	mathematical	—	`IsCoprime` `CommRing.toCommSemiring` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`abs_left_iff` `abs_right_iff`
`abs_left` 📖	mathematical	`IsCoprime` `CommRing.toCommSemiring`	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`abs_left_iff`
`abs_left_iff` 📖	mathematical	—	`IsCoprime` `CommRing.toCommSemiring` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`le_or_gt` `abs_of_nonneg` `abs_of_neg` `neg_left_iff`
`abs_right` 📖	mathematical	`IsCoprime` `CommRing.toCommSemiring`	`abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`abs_right_iff`
`abs_right_iff` 📖	mathematical	—	`IsCoprime` `CommRing.toCommSemiring` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`isCoprime_comm` `abs_left_iff`
`add_mul_left_left` 📖	mathematical	`IsCoprime` `CommRing.toCommSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`of_add_mul_left_left` `mul_neg` `add_neg_cancel_right`
`add_mul_left_left_iff` 📖	mathematical	—	`IsCoprime` `CommRing.toCommSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`of_add_mul_left_left` `add_mul_left_left`
`add_mul_left_right` 📖	mathematical	`IsCoprime` `CommRing.toCommSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`isCoprime_comm` `add_mul_left_left` `symm`
`add_mul_left_right_iff` 📖	mathematical	—	`IsCoprime` `CommRing.toCommSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`of_add_mul_left_right` `add_mul_left_right`
`add_mul_right_left` 📖	mathematical	`IsCoprime` `CommRing.toCommSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`mul_comm` `add_mul_left_left`
`add_mul_right_left_iff` 📖	mathematical	—	`IsCoprime` `CommRing.toCommSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`of_add_mul_right_left` `add_mul_right_left`
`add_mul_right_right` 📖	mathematical	`IsCoprime` `CommRing.toCommSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`isCoprime_comm` `add_mul_right_left` `symm`
`add_mul_right_right_iff` 📖	mathematical	—	`IsCoprime` `CommRing.toCommSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`of_add_mul_right_right` `add_mul_right_right`
`dvd_of_dvd_mul_left` 📖	—	`IsCoprime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	—	`one_mul` `add_mul` `Distrib.rightDistribClass` `mul_right_comm` `mul_assoc` `dvd_add` `Distrib.leftDistribClass` `dvd_mul_left` `Dvd.dvd.mul_left`
`dvd_of_dvd_mul_right` 📖	—	`IsCoprime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	—	`mul_one` `mul_add` `Distrib.leftDistribClass` `mul_assoc` `mul_left_comm` `dvd_add` `dvd_mul_left` `Dvd.dvd.mul_left`
`intCast` 📖	mathematical	`IsCoprime` `Int.instCommSemiring`	`CommRing.toCommSemiring` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Nat.cast_one` `Int.cast_one`
`isRelPrime` 📖	mathematical	`IsCoprime`	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	—	`isUnit_of_dvd'`
`isUnit_of_dvd` 📖	mathematical	`IsCoprime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring`	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	—	`isCoprime_self` `of_mul_right_left`
`isUnit_of_dvd'` 📖	mathematical	`IsCoprime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring`	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	—	`isUnit_of_dvd` `of_isCoprime_of_dvd_left`
`map` 📖	mathematical	`IsCoprime`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike`	—	`RingHom.map_mul` `RingHom.map_add` `RingHom.map_one`
`mono` 📖	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `IsCoprime`	—	—	`of_isCoprime_of_dvd_right` `of_isCoprime_of_dvd_left`
`mul_add_left_left` 📖	mathematical	`IsCoprime` `CommRing.toCommSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`add_comm` `add_mul_left_left`
`mul_add_left_left_iff` 📖	mathematical	—	`IsCoprime` `CommRing.toCommSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`of_mul_add_left_left` `mul_add_left_left`
`mul_add_left_right` 📖	mathematical	`IsCoprime` `CommRing.toCommSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`add_comm` `add_mul_left_right`
`mul_add_left_right_iff` 📖	mathematical	—	`IsCoprime` `CommRing.toCommSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`of_mul_add_left_right` `mul_add_left_right`
`mul_add_right_left` 📖	mathematical	`IsCoprime` `CommRing.toCommSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`add_comm` `add_mul_right_left`
`mul_add_right_left_iff` 📖	mathematical	—	`IsCoprime` `CommRing.toCommSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`of_mul_add_right_left` `mul_add_right_left`
`mul_add_right_right` 📖	mathematical	`IsCoprime` `CommRing.toCommSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`add_comm` `add_mul_right_right`
`mul_add_right_right_iff` 📖	mathematical	—	`IsCoprime` `CommRing.toCommSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`of_mul_add_right_right` `mul_add_right_right`
`mul_dvd` 📖	mathematical	`IsCoprime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`mul_one` `mul_add` `Distrib.leftDistribClass` `dvd_add` `mul_comm` `mul_assoc` `Dvd.dvd.mul_left` `mul_dvd_mul_left` `Dvd.dvd.mul_right` `mul_dvd_mul_right`
`mul_left` 📖	mathematical	`IsCoprime`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `mul_one`
`mul_left_iff` 📖	mathematical	—	`IsCoprime` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`of_mul_left_left` `of_mul_left_right` `mul_left`
`mul_right` 📖	mathematical	`IsCoprime`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`isCoprime_comm` `mul_left`
`mul_right_iff` 📖	mathematical	—	`IsCoprime` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`isCoprime_comm` `mul_left_iff`
`ne_zero` 📖	—	`IsCoprime`	—	—	`not_isCoprime_zero_zero`
`ne_zero_or_ne_zero` 📖	—	`IsCoprime`	—	—	`not_or_of_imp` `not_isCoprime_zero_zero`
`neg_left` 📖	mathematical	`IsCoprime` `CommRing.toCommSemiring`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`neg_mul_neg`
`neg_left_iff` 📖	mathematical	—	`IsCoprime` `CommRing.toCommSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`neg_left` `neg_neg`
`neg_neg` 📖	mathematical	`IsCoprime` `CommRing.toCommSemiring`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`neg_right` `neg_left`
`neg_neg_iff` 📖	mathematical	—	`IsCoprime` `CommRing.toCommSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`neg_left_iff` `neg_right_iff`
`neg_right` 📖	mathematical	`IsCoprime` `CommRing.toCommSemiring`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`symm` `neg_left`
`neg_right_iff` 📖	mathematical	—	`IsCoprime` `CommRing.toCommSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`neg_right` `neg_neg`
`of_add_mul_left_left` 📖	—	`IsCoprime` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toMul`	—	—	`mul_comm` `add_comm` `mul_add` `Distrib.leftDistribClass` `mul_left_comm` `add_left_comm`
`of_add_mul_left_right` 📖	—	`IsCoprime` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toMul`	—	—	`isCoprime_comm` `of_add_mul_left_left`
`of_add_mul_right_left` 📖	—	`IsCoprime` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toMul`	—	—	`of_add_mul_left_left` `mul_comm`
`of_add_mul_right_right` 📖	—	`IsCoprime` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toMul`	—	—	`of_add_mul_left_right` `mul_comm`
`of_isCoprime_of_dvd_left` 📖	—	`IsCoprime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring`	—	—	`of_mul_left_left`
`of_isCoprime_of_dvd_right` 📖	—	`IsCoprime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring`	—	—	`symm` `of_isCoprime_of_dvd_left`
`of_mul_add_left_left` 📖	—	`IsCoprime` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toMul`	—	—	`of_add_mul_left_left` `add_comm`
`of_mul_add_left_right` 📖	—	`IsCoprime` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toMul`	—	—	`of_add_mul_left_right` `add_comm`
`of_mul_add_right_left` 📖	—	`IsCoprime` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toMul`	—	—	`of_add_mul_right_left` `add_comm`
`of_mul_add_right_right` 📖	—	`IsCoprime` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toMul`	—	—	`of_add_mul_right_right` `add_comm`
`of_mul_left_left` 📖	—	`IsCoprime` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	—	`mul_right_comm` `mul_assoc`
`of_mul_left_right` 📖	—	`IsCoprime` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	—	`of_mul_left_left` `mul_comm`
`of_mul_right_left` 📖	—	`IsCoprime` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	—	`isCoprime_comm` `of_mul_left_left`
`of_mul_right_right` 📖	—	`IsCoprime` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	—	`of_mul_right_left` `mul_comm`
`sq_add_sq_ne_zero` 📖	—	`IsCoprime` `CommRing.toCommSemiring`	—	—	`add_eq_zero_iff_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `covariant_swap_add_of_covariant_add` `sq_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `not_isCoprime_zero_zero` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `eq_zero_of_pow_eq_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors`

IsRelPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_mul_left_left` 📖	mathematical	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`of_add_mul_left_left` `mul_neg` `add_neg_cancel_right`
`add_mul_left_left_iff` 📖	mathematical	—	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`of_add_mul_left_left` `add_mul_left_left`
`add_mul_left_right` 📖	mathematical	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`symm` `add_mul_left_left`
`add_mul_left_right_iff` 📖	mathematical	—	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`of_add_mul_left_right` `add_mul_left_right`
`add_mul_right_left` 📖	mathematical	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`add_mul_left_left` `mul_comm`
`add_mul_right_left_iff` 📖	mathematical	—	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`of_add_mul_right_left` `add_mul_right_left`
`add_mul_right_right` 📖	mathematical	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`symm` `add_mul_right_left`
`add_mul_right_right_iff` 📖	mathematical	—	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`of_add_mul_right_right` `add_mul_right_right`
`mul_add_left_left` 📖	mathematical	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`add_mul_left_left` `add_comm`
`mul_add_left_left_iff` 📖	mathematical	—	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`of_mul_add_left_left` `mul_add_left_left`
`mul_add_left_right` 📖	mathematical	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`add_mul_left_right` `add_comm`
`mul_add_left_right_iff` 📖	mathematical	—	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`of_mul_add_left_right` `mul_add_left_right`
`mul_add_right_left` 📖	mathematical	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`add_mul_right_left` `add_comm`
`mul_add_right_left_iff` 📖	mathematical	—	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`of_mul_add_right_left` `mul_add_right_left`
`mul_add_right_right` 📖	mathematical	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`add_mul_right_right` `add_comm`
`mul_add_right_right_iff` 📖	mathematical	—	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul`	—	`of_mul_add_right_right` `mul_add_right_right`
`neg_left` 📖	mathematical	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`dvd_neg`
`neg_left_iff` 📖	mathematical	—	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`neg_left` `neg_neg`
`neg_neg` 📖	mathematical	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`neg_right` `neg_left`
`neg_neg_iff` 📖	mathematical	—	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`neg_left_iff` `neg_right_iff`
`neg_right` 📖	mathematical	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`symm` `neg_left`
`neg_right_iff` 📖	mathematical	—	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`neg_right` `neg_neg`
`of_add_mul_left_left` 📖	—	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul`	—	—	`dvd_add` `Distrib.leftDistribClass` `dvd_mul_of_dvd_left`
`of_add_mul_left_right` 📖	—	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul`	—	—	`isRelPrime_comm` `of_add_mul_left_left`
`of_add_mul_right_left` 📖	—	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul`	—	—	`of_add_mul_left_left` `mul_comm`
`of_add_mul_right_right` 📖	—	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul`	—	—	`of_add_mul_left_right` `mul_comm`
`of_mul_add_left_left` 📖	—	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul`	—	—	`of_add_mul_left_left` `add_comm`
`of_mul_add_left_right` 📖	—	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul`	—	—	`of_add_mul_left_right` `add_comm`
`of_mul_add_right_left` 📖	—	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul`	—	—	`of_add_mul_right_left` `add_comm`
`of_mul_add_right_right` 📖	—	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul`	—	—	`of_add_mul_right_right` `add_comm`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoprime_iff` 📖	mathematical	—	`IsCoprime` `instCommSemiring`	—	`Unique.instSubsingleton` `isCoprime_one_left` `isCoprime_one_right`

PNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoprime_iff` 📖	mathematical	—	`IsCoprime` `Nat.instCommSemiring` `val` `PNat` `instOfNatPNatOfNeZeroNat`	—	—

Semifield

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoprime_iff` 📖	mathematical	—	`IsCoprime` `toCommSemiring`	—	`eq_or_ne` `MulZeroClass.zero_mul` `inv_mul_cancel₀` `zero_add`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoprime_comm` 📖	mathematical	—	`IsCoprime`	—	`IsCoprime.symm`
`isCoprime_group_smul` 📖	mathematical	—	`IsCoprime` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`isCoprime_group_smul_left` `isCoprime_group_smul_right`
`isCoprime_group_smul_left` 📖	mathematical	—	`IsCoprime` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`smul_mul_assoc` `mul_smul_comm` `smul_mul_smul_comm` `IsScalarTower.left` `inv_mul_cancel` `one_smul`
`isCoprime_group_smul_right` 📖	mathematical	—	`IsCoprime` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`isCoprime_comm` `isCoprime_group_smul_left`
`isCoprime_mul_unit_left` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`IsCoprime` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`isCoprime_mul_units_left`
`isCoprime_mul_unit_left_left` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`IsCoprime` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`isCoprime_group_smul_left` `Units.smulCommClass_left` `smulCommClass_self` `Units.instIsScalarTower` `IsScalarTower.left`
`isCoprime_mul_unit_left_right` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`IsCoprime` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`isCoprime_group_smul_right` `Units.smulCommClass_left` `smulCommClass_self` `Units.instIsScalarTower` `IsScalarTower.left`
`isCoprime_mul_unit_right` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`IsCoprime` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`isCoprime_mul_units_right`
`isCoprime_mul_unit_right_left` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`IsCoprime` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`isCoprime_mul_unit_left_left` `mul_comm`
`isCoprime_mul_unit_right_right` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`IsCoprime` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`isCoprime_mul_unit_left_right` `mul_comm`
`isCoprime_mul_units_left` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`IsCoprime` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`isCoprime_mul_unit_left_left` `isCoprime_mul_unit_left_right`
`isCoprime_mul_units_right` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`IsCoprime` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`isCoprime_mul_unit_right_left` `isCoprime_mul_unit_right_right`
`isCoprime_one_left` 📖	mathematical	—	`IsCoprime` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`one_mul` `MulZeroClass.zero_mul` `add_zero`
`isCoprime_one_right` 📖	mathematical	—	`IsCoprime` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`one_mul` `MulZeroClass.zero_mul` `zero_add`
`isCoprime_self` 📖	mathematical	—	`IsCoprime` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	—	`IsUnit.of_mul_eq_one` `instIsDedekindFiniteMonoid` `mul_comm` `add_mul` `Distrib.rightDistribClass` `isUnit_iff_exists_inv'` `MulZeroClass.zero_mul` `add_zero`
`isCoprime_zero_left` 📖	mathematical	—	`IsCoprime` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`IsUnit.of_mul_eq_one` `instIsDedekindFiniteMonoid` `mul_comm` `zero_add` `MulZeroClass.mul_zero` `isUnit_iff_exists_inv'` `one_mul`
`isCoprime_zero_right` 📖	mathematical	—	`IsCoprime` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`isCoprime_comm` `isCoprime_zero_left`
`not_isCoprime_zero_zero` 📖	mathematical	—	`IsCoprime` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`isCoprime_zero_right` `not_isUnit_zero`

---

← Back to Index