CancelMulZero

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

Statistics

Metric	Count
Definitions	0
Theorems isCancelMulZero, isLeftCancelMulZero, isRightCancelMulZero	3
Total	3

MulZeroMemClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCancelMulZero 📖	mathematical	—	IsCancelMulZero SetLike.instMembership MulMemClass.mul ZeroMemClass.zero	—	isLeftCancelMulZero IsCancelMulZero.toIsLeftCancelMulZero isRightCancelMulZero IsCancelMulZero.toIsRightCancelMulZero
isLeftCancelMulZero 📖	mathematical	—	IsLeftCancelMulZero SetLike.instMembership MulMemClass.mul ZeroMemClass.zero	—	Function.Injective.isLeftCancelMulZero Subtype.coe_injective
isRightCancelMulZero 📖	mathematical	—	IsRightCancelMulZero SetLike.instMembership MulMemClass.mul ZeroMemClass.zero	—	Function.Injective.isRightCancelMulZero Subtype.coe_injective

---

← Back to Index