Theorems · Definition · order theory
OrderIso.mulRight
{α : Type u} → [inst : Group α] → [inst_1 : LE α] → [MulRightMono α] → α → α ≃o αEquiv.mulRight as an OrderIso. See also OrderEmbedding.mulRight.
- Defined in
- Mathlib.Algebra.Order.Group.OrderIso
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Quot.sound
- Assumes
- GroupLEMulRightMono
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivproof · cited by 8,337
- Groupstatement and proof · cited by 6,238
- OrderIsostatement · cited by 874
- MulRightMonostatement and proof · cited by 263
- Equiv.mulRightproof · cited by 21
Cited by14
Results whose statement or proof uses this declaration.
- sup_mulproof · cited by 3
- inf_mulproof · cited by 2
- IsLUB.mulproof · cited by 2
- sSup_mulproof · cited by 1
- csSup_mulproof · cited by 1
- csInf_mulproof · cited by 1
- ciSup_mulproof · cited by 1
- ciInf_mulproof · cited by 1
- sInf_mulproof · cited by 1
- OrderIso.mulRight_applystatement and proof · cited by 0
- OrderIso.mulRight_symmstatement and proof · cited by 0
- OrderIso.mulRight_toEquivstatement and proof · cited by 0