Documentation Verification Report

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`	`IsAddLeftRegular` `Prod.instAdd`	—	—

IsAddRegular

Theorems

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

IsAddRightRegular

Theorems

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

IsLeftRegular

Theorems

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

IsRegular

Theorems

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

IsRightRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prodMk` 📖	mathematical	`IsRightRegular`	`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