Finset

📁 Source: Mathlib/Algebra/Ring/Pointwise/Finset.lean

Statistics

Metric	Count
Definitions distribNeg	1
Theorems add_mul_subset, mul_add_subset	2
Total	3

Finset

Definitions

Name	Category	Theorems
distribNeg 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_mul_subset 📖	mathematical	—	Finset instHasSubset mul Distrib.toMul add Distrib.toAdd	—	image₂_distrib_subset_right add_mul Distrib.rightDistribClass
mul_add_subset 📖	mathematical	—	Finset instHasSubset mul Distrib.toMul add Distrib.toAdd	—	image₂_distrib_subset_left mul_add Distrib.leftDistribClass

---

← Back to Index