Documentation Verification Report

Instances

📁 Source: Mathlib/Algebra/GroupWithZero/Submonoid/Instances.lean

Statistics

Metric	Count
Definitions `instCommGroupWithZeroSubtypeMemSubmonoidMrange`, `instCommMonoidWithZeroSubtypeMemSubmonoidMrange`, `instGroupWithZeroSubtypeMemSubmonoidMrange`, `instMonoidWithZeroSubtypeMemSubmonoidMrange`, `instMulZeroOneClassSubtypeMemSubmonoidMrange`	5
Theorems `val_mrange_zero`	1
Total	6

MonoidWithZeroHom

Definitions

Name	Category	Theorems
`instCommGroupWithZeroSubtypeMemSubmonoidMrange` 📖	CompOp	—
`instCommMonoidWithZeroSubtypeMemSubmonoidMrange` 📖	CompOp	—
`instGroupWithZeroSubtypeMemSubmonoidMrange` 📖	CompOp	—
`instMonoidWithZeroSubtypeMemSubmonoidMrange` 📖	CompOp	—
`instMulZeroOneClassSubtypeMemSubmonoidMrange` 📖	CompOp	1 math math: `val_mrange_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`val_mrange_zero` 📖	mathematical	—	`Submonoid` `MulZeroOneClass.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `MonoidHom.mrange` `MonoidWithZeroHom` `funLike` `MonoidWithZeroHomClass.toMonoidHomClass` `monoidWithZeroHomClass` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `instMulZeroOneClassSubtypeMemSubmonoidMrange`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `monoidWithZeroHomClass`

---

← Back to Index