OrderIso

📁 Source: Mathlib/Algebra/Order/Group/OrderIso.lean

Statistics

Metric	Count
Definitions `addLeft`, `addRight`, `divLeft`, `divRight`, `inv`, `mulLeft`, `mulRight`, `neg`, `subLeft`, `subRight`	10
Theorems `addLeft_apply`, `addLeft_symm`, `addLeft_toEquiv`, `addRight_apply`, `addRight_symm`, `addRight_toEquiv`, `divLeft_apply`, `divLeft_symm_apply`, `divRight_apply`, `divRight_symm_apply`, `inv_apply`, `inv_symm_apply`, `mulLeft_apply`, `mulLeft_symm`, `mulLeft_toEquiv`, `mulRight_apply`, `mulRight_symm`, `mulRight_toEquiv`, `neg_apply`, `neg_symm_apply`, `subLeft_apply`, `subLeft_symm_apply`, `subRight_apply`, `subRight_symm_apply`, `inv_le'`, `inv_le_of_inv_le'`, `le_inv'`, `le_inv_of_le_inv`, `le_neg`, `le_neg_of_le_neg`, `neg_le`, `neg_le_of_neg_le`	32
Total	42

OrderIso

Definitions

Name	Category	Theorems
`addLeft` 📖	CompOp	3 math math: `addLeft_symm`, `addLeft_toEquiv`, `addLeft_apply`
`addRight` 📖	CompOp	3 math math: `addRight_apply`, `addRight_toEquiv`, `addRight_symm`
`divLeft` 📖	CompOp	2 math math: `divLeft_apply`, `divLeft_symm_apply`
`divRight` 📖	CompOp	2 math math: `divRight_symm_apply`, `divRight_apply`
`inv` 📖	CompOp	2 math math: `inv_symm_apply`, `inv_apply`
`mulLeft` 📖	CompOp	3 math math: `mulLeft_symm`, `mulLeft_toEquiv`, `mulLeft_apply`
`mulRight` 📖	CompOp	3 math math: `mulRight_toEquiv`, `mulRight_symm`, `mulRight_apply`
`neg` 📖	CompOp	2 math math: `neg_apply`, `neg_symm_apply`
`subLeft` 📖	CompOp	2 math math: `subLeft_apply`, `subLeft_symm_apply`
`subRight` 📖	CompOp	2 math math: `subRight_symm_apply`, `subRight_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLeft_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `RelIso.instFunLike` `addLeft` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—
`addLeft_symm` 📖	mathematical	—	`symm` `addLeft` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`ext`
`addLeft_toEquiv` 📖	mathematical	—	`RelIso.toEquiv` `addLeft` `Equiv.addLeft`	—	—
`addRight_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `RelIso.instFunLike` `addRight` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—
`addRight_symm` 📖	mathematical	—	`symm` `addRight` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`ext`
`addRight_toEquiv` 📖	mathematical	—	`RelIso.toEquiv` `addRight` `Equiv.addRight`	—	—
`divLeft_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `OrderDual` `OrderDual.instLE` `RelIso.instFunLike` `divLeft` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	—
`divLeft_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `OrderDual` `OrderDual.instLE` `RelIso.instFunLike` `RelIso.symm` `divLeft` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	—
`divRight_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `RelIso.instFunLike` `divRight` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	—
`divRight_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `RelIso.instFunLike` `RelIso.symm` `divRight` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`inv_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `OrderDual` `OrderDual.instLE` `RelIso.instFunLike` `inv` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `InvolutiveInv.toInv` `DivisionMonoid.toInvolutiveInv` `Group.toDivisionMonoid`	—	—
`inv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `OrderDual` `OrderDual.instLE` `RelIso.instFunLike` `RelIso.symm` `inv` `InvolutiveInv.toInv` `DivisionMonoid.toInvolutiveInv` `Group.toDivisionMonoid` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	—
`mulLeft_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `RelIso.instFunLike` `mulLeft` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`mulLeft_symm` 📖	mathematical	—	`symm` `mulLeft` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`ext`
`mulLeft_toEquiv` 📖	mathematical	—	`RelIso.toEquiv` `mulLeft` `Equiv.mulLeft`	—	—
`mulRight_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `RelIso.instFunLike` `mulRight` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`mulRight_symm` 📖	mathematical	—	`symm` `mulRight` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`ext`
`mulRight_toEquiv` 📖	mathematical	—	`RelIso.toEquiv` `mulRight` `Equiv.mulRight`	—	—
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `OrderDual` `OrderDual.instLE` `RelIso.instFunLike` `neg` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `InvolutiveNeg.toNeg` `SubtractionMonoid.toInvolutiveNeg` `AddGroup.toSubtractionMonoid`	—	—
`neg_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `OrderDual` `OrderDual.instLE` `RelIso.instFunLike` `RelIso.symm` `neg` `InvolutiveNeg.toNeg` `SubtractionMonoid.toInvolutiveNeg` `AddGroup.toSubtractionMonoid` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	—
`subLeft_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `OrderDual` `OrderDual.instLE` `RelIso.instFunLike` `subLeft` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	—
`subLeft_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `OrderDual` `OrderDual.instLE` `RelIso.instFunLike` `RelIso.symm` `subLeft` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	—
`subRight_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `RelIso.instFunLike` `subRight` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	—
`subRight_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `RelIso.instFunLike` `RelIso.symm` `subRight` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inv_le'` 📖	mathematical	—	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`OrderIso.symm_apply_le`
`inv_le_of_inv_le'` 📖	—	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—	`inv_le'`
`le_inv'` 📖	mathematical	—	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`OrderIso.le_symm_apply`
`le_inv_of_le_inv` 📖	—	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—	`le_inv'`
`le_neg` 📖	mathematical	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`OrderIso.le_symm_apply`
`le_neg_of_le_neg` 📖	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—	`le_neg`
`neg_le` 📖	mathematical	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`OrderIso.symm_apply_le`
`neg_le_of_neg_le` 📖	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—	`neg_le`

---

← Back to Index