Documentation Verification Report

BigOperators

📁 Source: Mathlib/Data/Nat/GCD/BigOperators.lean

Statistics

Metric	Count
Definitions	0
Theorems `prod_left`, `prod_right`, `coprime_fintype_prod_left_iff`, `coprime_fintype_prod_right_iff`, `coprime_list_prod_left_iff`, `coprime_list_prod_right_iff`, `coprime_multiset_prod_left_iff`, `coprime_multiset_prod_right_iff`, `coprime_prod_left_iff`, `coprime_prod_right_iff`	10
Total	10

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coprime_fintype_prod_left_iff` 📖	mathematical	—	`Finset.prod` `instCommMonoid` `Finset.univ`	—	—
`coprime_fintype_prod_right_iff` 📖	mathematical	—	`Finset.prod` `instCommMonoid` `Finset.univ`	—	—
`coprime_list_prod_left_iff` 📖	mathematical	—	`instOne`	—	`instIsEmptyFalse`
`coprime_list_prod_right_iff` 📖	mathematical	—	`instOne`	—	—
`coprime_multiset_prod_left_iff` 📖	mathematical	—	`Multiset.prod` `instCommMonoid`	—	`coprime_list_prod_left_iff`
`coprime_multiset_prod_right_iff` 📖	mathematical	—	`Multiset.prod` `instCommMonoid`	—	`coprime_list_prod_right_iff`
`coprime_prod_left_iff` 📖	mathematical	—	`Finset.prod` `instCommMonoid`	—	`coprime_multiset_prod_left_iff`
`coprime_prod_right_iff` 📖	mathematical	—	`Finset.prod` `instCommMonoid`	—	`coprime_multiset_prod_right_iff`

Nat.Coprime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_left` 📖	mathematical	—	`Finset.prod` `Nat.instCommMonoid`	—	`Nat.coprime_prod_left_iff`
`prod_right` 📖	mathematical	—	`Finset.prod` `Nat.instCommMonoid`	—	`Nat.coprime_prod_right_iff`

---

← Back to Index