Documentation Verification Report

Lemmas

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

Statistics

Metric	Count
Definitions `instDecidableRelIntIsCoprime`	1
Theorems `prod_dvd_of_coprime`, `prod_dvd_of_isRelPrime`, `prod_dvd_of_coprime`, `prod_dvd_of_isRelPrime`, `isCoprime_gcdA`, `isCoprime_gcdB`, `isCoprime_iff_gcd_eq_one`, `natCoprime`, `nat_coprime`, `of_prod_left`, `of_prod_right`, `pow`, `pow_iff`, `pow_left`, `pow_left_iff`, `pow_right`, `pow_right_iff`, `prod_left`, `prod_left_iff`, `prod_right`, `prod_right_iff`, `of_prod_left`, `of_prod_right`, `pow`, `pow_iff`, `pow_left`, `pow_left_iff`, `pow_right`, `pow_right_iff`, `prod_left`, `prod_left_iff`, `prod_right`, `prod_right_iff`, `cast`, `isCoprime`, `isCoprime_iff_coprime`, `isCoprime_num_den`, `exists_sum_eq_one_iff_pairwise_coprime`, `exists_sum_eq_one_iff_pairwise_coprime'`, `ne_zero_or_ne_zero_of_nat_coprime`, `pairwise_coprime_iff_coprime_prod`, `pairwise_isRelPrime_iff_isRelPrime_prod`	42
Total	43

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_dvd_of_coprime` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `IsCoprime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring`	`prod` `CommSemiring.toCommMonoid`	—	`induction_on` `prod_insert` `IsCoprime.mul_dvd` `IsCoprime.prod_right` `coe_insert` `mem_insert_self` `Set.Pairwise.mono` `mem_insert_of_mem`
`prod_dvd_of_isRelPrime` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `IsRelPrime` `CommMonoid.toMonoid` `semigroupDvd` `Monoid.toSemigroup`	`prod`	—	`induction_on` `one_dvd` `prod_insert` `mem_insert_self` `IsRelPrime.mul_dvd` `IsRelPrime.prod_right` `mem_insert_of_mem` `Set.Pairwise.mono` `coe_insert`

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_dvd_of_coprime` 📖	mathematical	`Pairwise` `Function.onFun` `IsCoprime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring`	`Finset.prod` `CommSemiring.toCommMonoid` `Finset.univ`	—	`Finset.prod_dvd_of_coprime` `Pairwise.set_pairwise`
`prod_dvd_of_isRelPrime` 📖	mathematical	`Pairwise` `Function.onFun` `IsRelPrime` `CommMonoid.toMonoid` `semigroupDvd` `Monoid.toSemigroup`	`Finset.prod` `Finset.univ`	—	`Finset.prod_dvd_of_isRelPrime` `Pairwise.set_pairwise`

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoprime_gcdA` 📖	mathematical	`IsCoprime` `instCommSemiring`	`gcdA`	—	`mul_comm` `gcd_eq_gcd_ab` `Nat.cast_eq_one` `instCharZero` `isCoprime_iff_gcd_eq_one`
`isCoprime_gcdB` 📖	mathematical	`IsCoprime` `instCommSemiring`	`gcdB`	—	`add_comm` `mul_comm` `gcd_eq_gcd_ab` `Nat.cast_eq_one` `instCharZero` `isCoprime_iff_gcd_eq_one`
`isCoprime_iff_gcd_eq_one` 📖	mathematical	—	`IsCoprime` `instCommSemiring`	—	`gcd_dvd_iff` `mul_comm` `IsCoprime.eq_1` `gcd_eq_gcd_ab` `Nat.cast_one`

IsCoprime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`natCoprime` 📖	—	`IsCoprime` `Int.instCommSemiring`	—	—	`Nat.isCoprime_iff_coprime`
`nat_coprime` 📖	—	`IsCoprime` `Int.instCommSemiring`	—	—	`natCoprime`
`of_prod_left` 📖	—	`IsCoprime` `Finset.prod` `CommSemiring.toCommMonoid` `Finset` `Finset.instMembership`	—	—	`prod_left_iff`
`of_prod_right` 📖	—	`IsCoprime` `Finset.prod` `CommSemiring.toCommMonoid` `Finset` `Finset.instMembership`	—	—	`prod_right_iff`
`pow` 📖	mathematical	`IsCoprime`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	—	`pow_right` `pow_left`
`pow_iff` 📖	mathematical	—	`IsCoprime` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	—	`pow_left_iff` `pow_right_iff`
`pow_left` 📖	mathematical	`IsCoprime`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	—	`Finset.card_range` `Finset.prod_const` `prod_left`
`pow_left_iff` 📖	mathematical	—	`IsCoprime` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	—	`of_prod_left` `Finset.prod_const` `Finset.card_range` `Finset.mem_range` `pow_left`
`pow_right` 📖	mathematical	`IsCoprime`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	—	`Finset.card_range` `Finset.prod_const` `prod_right`
`pow_right_iff` 📖	mathematical	—	`IsCoprime` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	—	`isCoprime_comm` `pow_left_iff`
`prod_left` 📖	mathematical	`IsCoprime`	`Finset.prod` `CommSemiring.toCommMonoid`	—	`Finset.cons_induction` `isCoprime_one_left` `Finset.prod_cons` `mul_left` `Finset.forall_mem_cons`
`prod_left_iff` 📖	mathematical	—	`IsCoprime` `Finset.prod` `CommSemiring.toCommMonoid`	—	`Finset.induction_on` `isCoprime_one_left` `instIsEmptyFalse` `Finset.prod_insert` `mul_left_iff` `Finset.forall_mem_insert`
`prod_right` 📖	mathematical	`IsCoprime`	`Finset.prod` `CommSemiring.toCommMonoid`	—	`prod_left`
`prod_right_iff` 📖	mathematical	—	`IsCoprime` `Finset.prod` `CommSemiring.toCommMonoid`	—	`prod_left_iff`

IsRelPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_prod_left` 📖	—	`IsRelPrime` `CommMonoid.toMonoid` `Finset.prod` `Finset` `Finset.instMembership`	—	—	`prod_left_iff`
`of_prod_right` 📖	—	`IsRelPrime` `CommMonoid.toMonoid` `Finset.prod` `Finset` `Finset.instMembership`	—	—	`prod_right_iff`
`pow` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid`	`Monoid.toNatPow`	—	`pow_right` `pow_left`
`pow_iff` 📖	mathematical	—	`IsRelPrime` `CommMonoid.toMonoid` `Monoid.toNatPow`	—	`pow_left_iff` `pow_right_iff`
`pow_left` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid`	`Monoid.toNatPow`	—	`Finset.card_range` `Finset.prod_const` `prod_left`
`pow_left_iff` 📖	mathematical	—	`IsRelPrime` `CommMonoid.toMonoid` `Monoid.toNatPow`	—	`of_prod_left` `Finset.prod_const` `Finset.card_range` `Finset.mem_range` `pow_left`
`pow_right` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid`	`Monoid.toNatPow`	—	`Finset.card_range` `Finset.prod_const` `prod_right`
`pow_right_iff` 📖	mathematical	—	`IsRelPrime` `CommMonoid.toMonoid` `Monoid.toNatPow`	—	`isRelPrime_comm` `pow_left_iff`
`prod_left` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid`	`Finset.prod`	—	`Finset.induction_on` `isRelPrime_one_left` `Finset.prod_insert` `mul_left` `Finset.forall_mem_insert`
`prod_left_iff` 📖	mathematical	—	`IsRelPrime` `CommMonoid.toMonoid` `Finset.prod`	—	`Finset.induction_on` `isRelPrime_one_left` `instIsEmptyFalse` `Finset.prod_insert` `mul_left_iff` `Finset.forall_mem_insert`
`prod_right` 📖	mathematical	`IsRelPrime` `CommMonoid.toMonoid`	`Finset.prod`	—	`prod_left`
`prod_right_iff` 📖	mathematical	—	`IsRelPrime` `CommMonoid.toMonoid` `Finset.prod`	—	`prod_left_iff`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoprime_iff_coprime` 📖	mathematical	—	`IsCoprime` `Int.instCommSemiring`	—	`Int.isCoprime_iff_gcd_eq_one`

Nat.Coprime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast` 📖	mathematical	—	`IsCoprime` `CommRing.toCommSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Int.cast_natCast` `IsCoprime.intCast` `isCoprime`
`isCoprime` 📖	mathematical	—	`IsCoprime` `Int.instCommSemiring`	—	`Nat.isCoprime_iff_coprime`

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoprime_num_den` 📖	mathematical	—	`IsCoprime` `Int.instCommSemiring`	—	`IsCoprime.of_isCoprime_of_dvd_left` `Nat.Coprime.cast`

(root)

Definitions

Name	Category	Theorems
`instDecidableRelIntIsCoprime` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_sum_eq_one_iff_pairwise_coprime` 📖	mathematical	`Finset.Nonempty`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Finset.prod` `CommSemiring.toCommMonoid` `Finset` `Finset.instSDiff` `Finset.instSingleton` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Pairwise` `SetLike.instMembership` `Finset.instSetLike` `Function.onFun` `IsCoprime`	—	`Finset.Nonempty.cons_induction` `Finset.sum_singleton` `Finset.prod_congr` `sdiff_self` `mul_one` `instIsEmptyFalse` `Finset.pairwise_cons'` `Finset.mem_sdiff` `Finset.mem_singleton` `Finset.mem_insert_self` `Finset.sum_add_distrib` `Finset.sum_pi_single'` `mul_assoc` `Finset.prod_eq_mul_prod_diff_singleton` `Finset.erase_insert` `Finset.sdiff_singleton_eq_erase` `Finset.cons_eq_insert` `Finset.sum_cons` `Finset.sum_congr` `Pi.single_eq_same` `Pi.single_eq_of_ne` `MulZeroClass.zero_mul` `Finset.prod_eq_prod_diff_singleton_mul` `mul_comm` `sdiff_sdiff_comm` `add_mul` `Distrib.rightDistribClass` `Finset.sum_mul` `IsCoprime.symm` `IsCoprime.prod_left` `Finset.mul_sum` `one_mul` `ite_mul`
`exists_sum_eq_one_iff_pairwise_coprime'` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Finset.prod` `CommSemiring.toCommMonoid` `Compl.compl` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Finset.instSingleton` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Pairwise` `Function.onFun` `IsCoprime`	—	`Finset.coe_univ` `exists_sum_eq_one_iff_pairwise_coprime` `Finset.univ_nonempty`
`ne_zero_or_ne_zero_of_nat_coprime` 📖	—	—	—	—	`IsCoprime.ne_zero_or_ne_zero` `map_natCast` `RingHom.instRingHomClass` `IsCoprime.map` `Nat.Coprime.isCoprime`
`pairwise_coprime_iff_coprime_prod` 📖	mathematical	—	`Pairwise` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Function.onFun` `IsCoprime` `Finset.prod` `CommSemiring.toCommMonoid` `Finset.instSDiff` `Finset.instSingleton`	—	`Finset.pairwise_subtype_iff_pairwise_finset'` `IsCoprime.prod_right_iff` `IsCoprime.symm` `Finset.mem_singleton` `Finset.mem_sdiff`
`pairwise_isRelPrime_iff_isRelPrime_prod` 📖	mathematical	—	`Pairwise` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Function.onFun` `IsRelPrime` `CommMonoid.toMonoid` `Finset.prod` `Finset.instSDiff` `Finset.instSingleton`	—	`IsRelPrime.prod_right_iff` `Finset.mem_singleton` `Finset.mem_sdiff`

---

← Back to Index