WithZero

📁 Source: Mathlib/Algebra/Ring/WithZero.lean

Statistics

Metric	Count
Definitions instDistrib, instSemiring	2
Theorems instLeftDistribClass, instRightDistribClass	2
Total	4

WithZero

Definitions

Name	Category	Theorems
instDistrib 📖	CompOp	—
instSemiring 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLeftDistribClass 📖	mathematical	—	LeftDistribClass WithZero MulZeroClass.toMul instMulZeroClass instAdd	—	left_distrib
instRightDistribClass 📖	mathematical	—	RightDistribClass WithZero MulZeroClass.toMul instMulZeroClass instAdd	—	MulZeroClass.mul_zero add_zero right_distrib

---

← Back to Index