Documentation Verification Report

Inverses

📁 Source: Mathlib/GroupTheory/Submonoid/Inverses.lean

Statistics

Metric	Count
Definitions `fromCommLeftNeg`, `fromLeftNeg`, `instAddCommGroupSubtypeMemAddSubmonoid`, `instAddGroupSubtypeMemAddSubmonoid`, `leftNeg`, `leftNegEquiv`, `fromCommLeftInv`, `fromLeftInv`, `instCommGroupSubtypeMemSubmonoid`, `instGroupSubtypeMemSubmonoid`, `leftInv`, `leftInvEquiv`	12
Theorems `coe_neg`, `addUnit_mem_leftNeg`, `add_fromLeftNeg`, `add_leftNegEquiv`, `add_leftNegEquiv_symm`, `fromCommLeftNeg_apply`, `fromLeftNeg_add`, `fromLeftNeg_eq_iff`, `fromLeftNeg_eq_neg`, `fromLeftNeg_leftNegEquiv_symm`, `fromLeftNeg_zero`, `leftNegEquiv_add`, `leftNegEquiv_apply`, `leftNegEquiv_symm_add`, `leftNegEquiv_symm_eq_neg`, `leftNegEquiv_symm_fromLeftNeg`, `leftNeg_eq_neg`, `leftNeg_le_isAddUnit`, `leftNeg_leftNeg_eq`, `leftNeg_leftNeg_le`, `coe_inv`, `fromCommLeftInv_apply`, `fromLeftInv_eq_iff`, `fromLeftInv_eq_inv`, `fromLeftInv_leftInvEquiv_symm`, `fromLeftInv_mul`, `fromLeftInv_one`, `leftInvEquiv_apply`, `leftInvEquiv_mul`, `leftInvEquiv_symm_eq_inv`, `leftInvEquiv_symm_fromLeftInv`, `leftInvEquiv_symm_mul`, `leftInv_eq_inv`, `leftInv_le_isUnit`, `leftInv_leftInv_eq`, `leftInv_leftInv_le`, `mul_fromLeftInv`, `mul_leftInvEquiv`, `mul_leftInvEquiv_symm`, `unit_mem_leftInv`	40
Total	52

AddSubmonoid

Definitions

Name	Category	Theorems
`fromCommLeftNeg` 📖	CompOp	2 math math: `fromCommLeftNeg_apply`, `leftNegEquiv_apply`
`fromLeftNeg` 📖	CompOp	8 math math: `fromLeftNeg_leftNegEquiv_symm`, `add_fromLeftNeg`, `fromLeftNeg_zero`, `fromCommLeftNeg_apply`, `leftNegEquiv_symm_fromLeftNeg`, `fromLeftNeg_add`, `fromLeftNeg_eq_neg`, `fromLeftNeg_eq_iff`
`instAddCommGroupSubtypeMemAddSubmonoid` 📖	CompOp	—
`instAddGroupSubtypeMemAddSubmonoid` 📖	CompOp	1 math math: `IsUnit.Submonoid.coe_neg`
`leftNeg` 📖	CompOp	19 math math: `addUnit_mem_leftNeg`, `fromLeftNeg_leftNegEquiv_symm`, `add_leftNegEquiv_symm`, `leftNegEquiv_add`, `add_fromLeftNeg`, `fromLeftNeg_zero`, `leftNeg_leftNeg_eq`, `add_leftNegEquiv`, `fromCommLeftNeg_apply`, `leftNegEquiv_symm_add`, `leftNegEquiv_symm_fromLeftNeg`, `leftNegEquiv_apply`, `fromLeftNeg_add`, `leftNeg_le_isAddUnit`, `leftNeg_eq_neg`, `leftNeg_leftNeg_le`, `fromLeftNeg_eq_neg`, `fromLeftNeg_eq_iff`, `leftNegEquiv_symm_eq_neg`
`leftNegEquiv` 📖	CompOp	8 math math: `fromLeftNeg_leftNegEquiv_symm`, `add_leftNegEquiv_symm`, `leftNegEquiv_add`, `add_leftNegEquiv`, `leftNegEquiv_symm_add`, `leftNegEquiv_symm_fromLeftNeg`, `leftNegEquiv_apply`, `leftNegEquiv_symm_eq_neg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addUnit_mem_leftNeg` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike` `AddUnits.val`	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike` `leftNeg` `AddUnits.val` `AddUnits` `AddUnits.instNeg`	—	`AddUnits.neg_val`
`add_fromLeftNeg` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddSubmonoid` `SetLike.instMembership` `instSetLike` `leftNeg` `fromLeftNeg` `AddZero.toZero`	—	`Subtype.prop`
`add_leftNegEquiv` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsAddUnit.addSubmonoid`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid` `SetLike.instMembership` `instSetLike` `leftNeg` `DFunLike.coe` `AddEquiv` `add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `leftNegEquiv` `AddZero.toZero`	—	`add_fromLeftNeg`
`add_leftNegEquiv_symm` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsAddUnit.addSubmonoid`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid` `SetLike.instMembership` `instSetLike` `leftNeg` `DFunLike.coe` `AddEquiv` `add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `leftNegEquiv` `AddZero.toZero`	—	`AddEquiv.apply_symm_apply` `leftNegEquiv_add`
`fromCommLeftNeg_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `instSetLike` `leftNeg` `AddZeroClass.toAddZero` `toAddZeroClass` `AddMonoidHom.instFunLike` `fromCommLeftNeg` `fromLeftNeg`	—	—
`fromLeftNeg_add` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid` `SetLike.instMembership` `instSetLike` `fromLeftNeg` `leftNeg` `AddZero.toZero`	—	`add_comm` `add_fromLeftNeg`
`fromLeftNeg_eq_iff` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `instSetLike` `fromLeftNeg` `AddZero.toAdd` `AddZeroClass.toAddZero` `leftNeg` `AddZero.toZero`	—	`leftNeg_le_isAddUnit` `Subtype.prop` `add_fromLeftNeg`
`fromLeftNeg_eq_neg` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.instMembership` `instSetLike` `fromLeftNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `leftNeg`	—	`AddLeftCancelSemigroup.toIsLeftCancelAdd` `add_neg_cancel` `add_fromLeftNeg`
`fromLeftNeg_leftNegEquiv_symm` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsAddUnit.addSubmonoid`	`fromLeftNeg` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddEquiv` `AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike` `leftNeg` `add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `leftNegEquiv`	—	`Equiv.right_inv`
`fromLeftNeg_zero` 📖	mathematical	—	`fromLeftNeg` `AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike` `leftNeg` `zero`	—	`zero_add` `add_fromLeftNeg`
`leftNegEquiv_add` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsAddUnit.addSubmonoid`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `AddEquiv` `leftNeg` `add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `leftNegEquiv` `AddZero.toZero`	—	`fromLeftNeg_add`
`leftNegEquiv_apply` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsAddUnit.addSubmonoid`	`DFunLike.coe` `AddEquiv` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `instSetLike` `leftNeg` `add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `leftNegEquiv` `ZeroHom.toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `toAddZeroClass` `AddMonoidHom.toZeroHom` `fromCommLeftNeg`	—	—
`leftNegEquiv_symm_add` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsAddUnit.addSubmonoid`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid` `SetLike.instMembership` `instSetLike` `leftNeg` `DFunLike.coe` `AddEquiv` `add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `leftNegEquiv` `AddZero.toZero`	—	`AddEquiv.apply_symm_apply` `add_leftNegEquiv`
`leftNegEquiv_symm_eq_neg` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsAddUnit.addSubmonoid`	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `instSetLike` `leftNeg` `DFunLike.coe` `AddEquiv` `add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `leftNegEquiv` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`AddLeftCancelSemigroup.toIsLeftCancelAdd` `add_neg_cancel` `add_leftNegEquiv_symm`
`leftNegEquiv_symm_fromLeftNeg` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsAddUnit.addSubmonoid`	`DFunLike.coe` `AddEquiv` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `instSetLike` `leftNeg` `add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `leftNegEquiv` `fromLeftNeg`	—	`Equiv.left_inv`
`leftNeg_eq_neg` 📖	mathematical	—	`leftNeg` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubmonoid` `AddMonoid.toAddZeroClass` `neg`	—	`ext` `mem_neg` `Subtype.prop` `neg_eq_of_add_eq_zero_right` `add_neg_cancel`
`leftNeg_le_isAddUnit` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `leftNeg` `IsAddUnit.addSubmonoid`	—	`add_comm`
`leftNeg_leftNeg_eq` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsAddUnit.addSubmonoid`	`leftNeg`	—	`le_antisymm` `leftNeg_leftNeg_le` `neg_neg` `addUnit_mem_leftNeg`
`leftNeg_leftNeg_le` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `leftNeg`	—	`add_zero` `add_assoc` `zero_add` `Subtype.prop`

AddSubmonoid.IsUnit.Submonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_neg` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `AddSubmonoid.instSetLike` `IsAddUnit.addSubmonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid` `AddUnits.val` `AddUnits` `AddUnits.instNeg` `IsAddUnit.addUnit` `Subtype.prop`	—	—

Submonoid

Definitions

Name	Category	Theorems
`fromCommLeftInv` 📖	CompOp	2 math math: `leftInvEquiv_apply`, `fromCommLeftInv_apply`
`fromLeftInv` 📖	CompOp	8 math math: `fromLeftInv_leftInvEquiv_symm`, `fromLeftInv_eq_iff`, `fromLeftInv_mul`, `leftInvEquiv_symm_fromLeftInv`, `fromLeftInv_one`, `fromCommLeftInv_apply`, `fromLeftInv_eq_inv`, `mul_fromLeftInv`
`instCommGroupSubtypeMemSubmonoid` 📖	CompOp	—
`instGroupSubtypeMemSubmonoid` 📖	CompOp	1 math math: `IsUnit.Submonoid.coe_inv`
`leftInv` 📖	CompOp	19 math math: `mul_leftInvEquiv`, `leftInvEquiv_symm_mul`, `fromLeftInv_leftInvEquiv_symm`, `leftInvEquiv_apply`, `leftInvEquiv_mul`, `leftInv_leftInv_le`, `fromLeftInv_eq_iff`, `leftInv_eq_inv`, `fromLeftInv_mul`, `leftInvEquiv_symm_eq_inv`, `leftInv_leftInv_eq`, `leftInv_le_isUnit`, `leftInvEquiv_symm_fromLeftInv`, `fromLeftInv_one`, `unit_mem_leftInv`, `fromCommLeftInv_apply`, `fromLeftInv_eq_inv`, `mul_fromLeftInv`, `mul_leftInvEquiv_symm`
`leftInvEquiv` 📖	CompOp	8 math math: `mul_leftInvEquiv`, `leftInvEquiv_symm_mul`, `fromLeftInv_leftInvEquiv_symm`, `leftInvEquiv_apply`, `leftInvEquiv_mul`, `leftInvEquiv_symm_eq_inv`, `leftInvEquiv_symm_fromLeftInv`, `mul_leftInvEquiv_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fromCommLeftInv_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `instSetLike` `leftInv` `MulOneClass.toMulOne` `toMulOneClass` `MonoidHom.instFunLike` `fromCommLeftInv` `fromLeftInv`	—	—
`fromLeftInv_eq_iff` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `instSetLike` `fromLeftInv` `MulOne.toMul` `MulOneClass.toMulOne` `leftInv` `MulOne.toOne`	—	`leftInv_le_isUnit` `Subtype.prop` `mul_fromLeftInv`
`fromLeftInv_eq_inv` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.instMembership` `instSetLike` `fromLeftInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `leftInv`	—	`LeftCancelSemigroup.toIsLeftCancelMul` `mul_inv_cancel` `mul_fromLeftInv`
`fromLeftInv_leftInvEquiv_symm` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsUnit.submonoid`	`fromLeftInv` `CommMonoid.toMonoid` `DFunLike.coe` `MulEquiv` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `instSetLike` `leftInv` `mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `leftInvEquiv`	—	`Equiv.right_inv`
`fromLeftInv_mul` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Submonoid` `SetLike.instMembership` `instSetLike` `fromLeftInv` `leftInv` `MulOne.toOne`	—	`mul_comm` `mul_fromLeftInv`
`fromLeftInv_one` 📖	mathematical	—	`fromLeftInv` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `instSetLike` `leftInv` `one`	—	`one_mul` `mul_fromLeftInv`
`leftInvEquiv_apply` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsUnit.submonoid`	`DFunLike.coe` `MulEquiv` `Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `instSetLike` `leftInv` `mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `leftInvEquiv` `OneHom.toFun` `MulOne.toOne` `MulOneClass.toMulOne` `toMulOneClass` `MonoidHom.toOneHom` `fromCommLeftInv`	—	—
`leftInvEquiv_mul` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsUnit.submonoid`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Submonoid` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `MulEquiv` `leftInv` `mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `leftInvEquiv` `MulOne.toOne`	—	`fromLeftInv_mul`
`leftInvEquiv_symm_eq_inv` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsUnit.submonoid`	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `CommGroup.toCommMonoid` `SetLike.instMembership` `instSetLike` `leftInv` `DFunLike.coe` `MulEquiv` `mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `leftInvEquiv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`LeftCancelSemigroup.toIsLeftCancelMul` `mul_inv_cancel` `mul_leftInvEquiv_symm`
`leftInvEquiv_symm_fromLeftInv` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsUnit.submonoid`	`DFunLike.coe` `MulEquiv` `Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `instSetLike` `leftInv` `mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `leftInvEquiv` `fromLeftInv`	—	`Equiv.left_inv`
`leftInvEquiv_symm_mul` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsUnit.submonoid`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Submonoid` `SetLike.instMembership` `instSetLike` `leftInv` `DFunLike.coe` `MulEquiv` `mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `leftInvEquiv` `MulOne.toOne`	—	`MulEquiv.apply_symm_apply` `mul_leftInvEquiv`
`leftInv_eq_inv` 📖	mathematical	—	`leftInv` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Submonoid` `Monoid.toMulOneClass` `inv`	—	`ext` `mem_inv` `Subtype.prop` `inv_eq_of_mul_eq_one_right` `mul_inv_cancel`
`leftInv_le_isUnit` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `leftInv` `IsUnit.submonoid`	—	`mul_comm`
`leftInv_leftInv_eq` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsUnit.submonoid`	`leftInv`	—	`le_antisymm` `leftInv_leftInv_le` `inv_inv` `unit_mem_leftInv`
`leftInv_leftInv_le` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `leftInv`	—	`mul_one` `mul_assoc` `one_mul` `Subtype.prop`
`mul_fromLeftInv` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Submonoid` `SetLike.instMembership` `instSetLike` `leftInv` `fromLeftInv` `MulOne.toOne`	—	`Subtype.prop`
`mul_leftInvEquiv` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsUnit.submonoid`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Submonoid` `SetLike.instMembership` `instSetLike` `leftInv` `DFunLike.coe` `MulEquiv` `mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `leftInvEquiv` `MulOne.toOne`	—	`mul_fromLeftInv`
`mul_leftInvEquiv_symm` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsUnit.submonoid`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Submonoid` `SetLike.instMembership` `instSetLike` `leftInv` `DFunLike.coe` `MulEquiv` `mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `leftInvEquiv` `MulOne.toOne`	—	`MulEquiv.apply_symm_apply` `leftInvEquiv_mul`
`unit_mem_leftInv` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `instSetLike` `Units.val`	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `instSetLike` `leftInv` `Units.val` `Units` `Units.instInv`	—	`Units.inv_val`

Submonoid.IsUnit.Submonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_inv` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `IsUnit.submonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Submonoid.instGroupSubtypeMemSubmonoid` `Units.val` `Units` `Units.instInv` `IsUnit.unit` `Subtype.prop`	—	—

---

← Back to Index