Invertible

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

Statistics

Metric	Count
Definitions invertibleDiv, invertibleInv, invertibleOfNonzero	3
Theorems ne_zero, toNeZero, inverse_invertible, div_mul_cancel_of_invertible, div_self_of_invertible, invOf_div, invOf_eq_inv, inv_mul_cancel_of_invertible, mul_div_cancel_of_invertible, mul_inv_cancel_of_invertible	10
Total	13

Invertible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ne_zero 📖	—	—	—	—	zero_ne_one NeZero.one MulZeroClass.mul_zero invOf_mul_self
toNeZero 📖	mathematical	—	MulZeroClass.toZero MulZeroOneClass.toMulZeroClass	—	ne_zero

Ring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inverse_invertible 📖	mathematical	—	inverse Invertible.invOf MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	inverse_unit

(root)

Definitions

Name	Category	Theorems
invertibleDiv 📖	CompOp	—
invertibleInv 📖	CompOp	—
invertibleOfNonzero 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
div_mul_cancel_of_invertible 📖	mathematical	—	MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid	—	div_mul_cancel₀ Invertible.ne_zero GroupWithZero.toNontrivial
div_self_of_invertible 📖	mathematical	—	DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	div_self Invertible.ne_zero GroupWithZero.toNontrivial
invOf_div 📖	mathematical	—	Invertible.invOf MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid	—	invOf_eq_right_inv div_mul_cancel_of_invertible div_self_of_invertible
invOf_eq_inv 📖	mathematical	—	Invertible.invOf MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid InvOneClass.toInv	—	invOf_eq_right_inv mul_inv_cancel₀ Invertible.ne_zero GroupWithZero.toNontrivial
inv_mul_cancel_of_invertible 📖	mathematical	—	MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid InvOneClass.toOne	—	inv_mul_cancel₀ Invertible.ne_zero GroupWithZero.toNontrivial
mul_div_cancel_of_invertible 📖	mathematical	—	DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	—	mul_div_cancel_right₀ GroupWithZero.toMulDivCancelClass Invertible.ne_zero GroupWithZero.toNontrivial
mul_inv_cancel_of_invertible 📖	mathematical	—	MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid InvOneClass.toOne	—	mul_inv_cancel₀ Invertible.ne_zero GroupWithZero.toNontrivial

---

← Back to Index