Documentation Verification Report

Equiv

📁 Source: Mathlib/Algebra/GroupWithZero/Equiv.lean

Statistics

Metric	Count
Definitions `toMonoidWithZeroHom`	1
Theorems `toMonoidWithZeroHom_apply`, `toMonoidWithZeroHom_bijective`, `toMonoidWithZeroHom_inj`, `toMonoidWithZeroHom_injective`, `toMonoidWithZeroHom_surjective`, `toMonoidWithZeroHomClass`, `toZeroHomClass`	7
Total	8

MulEquiv

Definitions

Name	Category	Theorems
`toMonoidWithZeroHom` 📖	CompOp	5 math math: `toMonoidWithZeroHom_apply`, `toMonoidWithZeroHom_injective`, `toMonoidWithZeroHom_inj`, `toMonoidWithZeroHom_bijective`, `toMonoidWithZeroHom_surjective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toMonoidWithZeroHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZeroHom.funLike` `toMonoidWithZeroHom` `MulEquiv` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `EquivLike.toFunLike` `instEquivLike`	—	—
`toMonoidWithZeroHom_bijective` 📖	mathematical	—	`Function.Bijective` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZeroHom.funLike` `toMonoidWithZeroHom`	—	`bijective`
`toMonoidWithZeroHom_inj` 📖	mathematical	—	`toMonoidWithZeroHom`	—	—
`toMonoidWithZeroHom_injective` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZeroHom.funLike` `toMonoidWithZeroHom`	—	`injective`
`toMonoidWithZeroHom_surjective` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZeroHom.funLike` `toMonoidWithZeroHom`	—	`surjective`

MulEquivClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toMonoidWithZeroHomClass` 📖	mathematical	—	`MonoidWithZeroHomClass` `EquivLike.toFunLike`	—	`instMonoidHomClass` `toZeroHomClass`
`toZeroHomClass` 📖	mathematical	—	`ZeroHomClass` `MulZeroClass.toZero` `EquivLike.toFunLike`	—	`map_mul` `MulZeroClass.zero_mul` `EquivLike.apply_inv_apply` `MulZeroClass.mul_zero`

---

← Back to Index