Lemmas

📁 Source: Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean

Statistics

Metric	Count
Definitions inverse, invMonoidWithZeroHom	2
Theorems div_eq_div_iff, inv_mul_eq_inv_mul_iff, mul_inv_eq_mul_inv_iff, coe_inverse, inverse_apply, eq_on_inv₀, instIsLocalHomOfMonoidWithZeroHomClassOfNontrivial, isLocalHom_of_exists_map_ne_one, map_div₀, map_eq_zero, map_inv₀, map_ne_zero, map_zpow₀	13
Total	15

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
div_eq_div_iff 📖	mathematical	Commute MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid	—	div_eq_div_iff_of_isUnit Ne.isUnit
inv_mul_eq_inv_mul_iff 📖	mathematical	Commute MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	inv_mul_eq_inv_mul_iff_of_isUnit Ne.isUnit
mul_inv_eq_mul_inv_iff 📖	mathematical	Commute MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	mul_inv_eq_mul_inv_iff_of_isUnit Ne.isUnit

MonoidWithZero

Definitions

Name	Category	Theorems
inverse 📖	CompOp	2 math math: coe_inverse, inverse_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_inverse 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero MonoidWithZeroHom.funLike inverse Ring.inverse	—	—
inverse_apply 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero MonoidWithZeroHom.funLike inverse Ring.inverse	—	—

(root)

Definitions

Name	Category	Theorems
invMonoidWithZeroHom 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_on_inv₀ 📖	mathematical	DFunLike.coe	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	eq_or_ne inv_zero map_zero MonoidWithZeroHomClass.toZeroHomClass IsUnit.eq_on_inv MonoidWithZeroHomClass.toMonoidHomClass
instIsLocalHomOfMonoidWithZeroHomClassOfNontrivial 📖	mathematical	—	IsLocalHom MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero	—	isLocalHom_of_exists_map_ne_one MonoidWithZeroHomClass.toMonoidHomClass map_zero MonoidWithZeroHomClass.toZeroHomClass NeZero.one
isLocalHom_of_exists_map_ne_one 📖	mathematical	—	IsLocalHom MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero	—	eq_or_ne map_mul MonoidHomClass.toMulHomClass IsUnit.mul_right_cancel MulZeroClass.mul_zero one_mul mul_inv_cancel₀ inv_mul_cancel₀
map_div₀ 📖	mathematical	—	DFunLike.coe DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid	—	map_div' MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass map_inv₀
map_eq_zero 📖	mathematical	—	DFunLike.coe MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	—	not_iff_not map_ne_zero
map_inv₀ 📖	mathematical	—	DFunLike.coe InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	inv_zero map_zero MonoidWithZeroHomClass.toZeroHomClass eq_inv_of_mul_eq_one_left map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass inv_mul_cancel₀ map_one MonoidHomClass.toOneHomClass
map_ne_zero 📖	—	—	—	—	map_zero MonoidWithZeroHomClass.toZeroHomClass CanLift.prf instCanLiftUnitsValIsUnit isUnit_iff_ne_zero one_ne_zero NeZero.one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass Units.mul_inv map_mul MonoidHomClass.toMulHomClass MulZeroClass.zero_mul
map_zpow₀ 📖	mathematical	—	DFunLike.coe DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid	—	map_zpow' MonoidWithZeroHomClass.toMonoidHomClass map_inv₀

---

← Back to Index