Documentation Verification Report

Opposite

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

Statistics

Metric	Count
Definitions `instGroupWithZero`, `instMonoidWithZero`, `instMulZeroClass`, `instMulZeroOneClass`, `instSemigroupWithZero`, `instGroupWithZero`, `instMonoidWithZero`, `instMulZeroClass`, `instMulZeroOneClass`, `instSemigroupWithZero`	10
Theorems `instNoZeroDivisors`, `instIsCancelMulZero`, `instIsLeftCancelMulZeroOfIsRightCancelMulZero`, `instIsRightCancelMulZeroOfIsLeftCancelMulZero`, `instNoZeroDivisors`, `isCancelMulZero_iff`, `isLeftCancelMulZero_iff`, `isRightCancelMulZero_iff`	8
Total	18

AddOpposite

Definitions

Name	Category	Theorems
`instGroupWithZero` 📖	CompOp	—
`instMonoidWithZero` 📖	CompOp	—
`instMulZeroClass` 📖	CompOp	—
`instMulZeroOneClass` 📖	CompOp	—
`instSemigroupWithZero` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNoZeroDivisors` 📖	mathematical	—	`NoZeroDivisors` `AddOpposite` `instMul` `instZero`	—	`unop_injective` `NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero` `op_injective`

MulOpposite

Definitions

Name	Category	Theorems
`instGroupWithZero` 📖	CompOp	—
`instMonoidWithZero` 📖	CompOp	1 math math: `NormedAddGroupHom.isCentralScalar`
`instMulZeroClass` 📖	CompOp	—
`instMulZeroOneClass` 📖	CompOp	—
`instSemigroupWithZero` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsCancelMulZero` 📖	mathematical	—	`IsCancelMulZero` `MulOpposite` `instMul` `instZero`	—	`instIsLeftCancelMulZeroOfIsRightCancelMulZero` `IsCancelMulZero.toIsRightCancelMulZero` `instIsRightCancelMulZeroOfIsLeftCancelMulZero` `IsCancelMulZero.toIsLeftCancelMulZero`
`instIsLeftCancelMulZeroOfIsRightCancelMulZero` 📖	mathematical	—	`IsLeftCancelMulZero` `MulOpposite` `instMul` `instZero`	—	`unop_injective` `mul_right_cancel₀`
`instIsRightCancelMulZeroOfIsLeftCancelMulZero` 📖	mathematical	—	`IsRightCancelMulZero` `MulOpposite` `instMul` `instZero`	—	`unop_injective` `mul_left_cancel₀`
`instNoZeroDivisors` 📖	mathematical	—	`NoZeroDivisors` `MulOpposite` `instMul` `instZero`	—	`NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero` `op_injective` `unop_injective`
`isCancelMulZero_iff` 📖	mathematical	—	`IsCancelMulZero` `MulOpposite` `instMul` `instZero`	—	`Function.Injective.isCancelMulZero` `op_injective` `instIsCancelMulZero`
`isLeftCancelMulZero_iff` 📖	mathematical	—	`IsLeftCancelMulZero` `MulOpposite` `instMul` `instZero` `IsRightCancelMulZero`	—	`Function.Injective.isRightCancelMulZero` `op_injective` `instIsRightCancelMulZeroOfIsLeftCancelMulZero` `instIsLeftCancelMulZeroOfIsRightCancelMulZero`
`isRightCancelMulZero_iff` 📖	mathematical	—	`IsRightCancelMulZero` `MulOpposite` `instMul` `instZero` `IsLeftCancelMulZero`	—	`Function.Injective.isLeftCancelMulZero` `op_injective` `instIsLeftCancelMulZeroOfIsRightCancelMulZero` `instIsRightCancelMulZeroOfIsLeftCancelMulZero`

---

← Back to Index