Prod

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

Statistics

Metric	Count
Definitions	0
Theorems sumMk, sumMk, sumMk, prodMk, prodMk, prodMk, isAddLeftRegular_mk, isAddRegular_mk, isAddRightRegular_mk, isLeftRegular_mk, isRegular_mk, isRightRegular_mk, isSMulRegular_iff	13
Total	13

IsAddLeftRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sumMk 📖	mathematical	IsAddLeftRegular	Prod.instAdd	—	—

IsAddRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sumMk 📖	mathematical	IsAddRegular	Prod.instAdd	—	—

IsAddRightRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sumMk 📖	mathematical	IsAddRightRegular	Prod.instAdd	—	—

IsLeftRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prodMk 📖	mathematical	IsLeftRegular	Prod.instMul	—	—

IsRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prodMk 📖	mathematical	IsRegular	Prod.instMul	—	—

IsRightRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prodMk 📖	mathematical	IsRightRegular	Prod.instMul	—	—

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAddLeftRegular_mk 📖	mathematical	—	IsAddLeftRegular instAdd	—	map_injective
isAddRegular_mk 📖	mathematical	—	IsAddRegular instAdd	—	isAddRegular_iff
isAddRightRegular_mk 📖	mathematical	—	IsAddRightRegular instAdd	—	map_injective
isLeftRegular_mk 📖	mathematical	—	IsLeftRegular instMul	—	map_injective
isRegular_mk 📖	mathematical	—	IsRegular instMul	—	—
isRightRegular_mk 📖	mathematical	—	IsRightRegular instMul	—	map_injective
isSMulRegular_iff 📖	mathematical	—	IsSMulRegular instSMul	—	map_injective

---

← Back to Index