Prod

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

Statistics

Metric	Count
Definitions	0
Theorems mk_dvd_mk, instDecompositionMonoidForall, instDecompositionMonoidProd, pi_dvd_iff, prod_dvd_iff	5
Total	5

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_dvd_mk 📖	mathematical	—	semigroupDvd instSemigroup	—	prod_dvd_iff

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDecompositionMonoidForall 📖	mathematical	DecompositionMonoid	Pi.semigroup	—	DecompositionMonoid.primal
instDecompositionMonoidProd 📖	mathematical	—	DecompositionMonoid Prod.instSemigroup	—	DecompositionMonoid.primal
pi_dvd_iff 📖	mathematical	—	semigroupDvd Pi.semigroup	—	—
prod_dvd_iff 📖	mathematical	—	semigroupDvd Prod.instSemigroup	—	—

---

← Back to Index