Mathlib Map

Theorems · Definition · order theory

OrderIso.addRight

{α : Type u} → [inst : AddGroup α] → [inst_1 : LE α] → [AddRightMono α] → α → α ≃o α

Equiv.addRight as an OrderIso. See also OrderEmbedding.addRight.

Defined in
Mathlib.Algebra.Order.Group.OrderIso
Cited by
16 results in Mathlib
Foundations
Depth 18 from the axioms · uses propext, Quot.sound
Assumes
AddGroupLEAddRightMono
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

csSup_add · cited by 3csSup_addsup_add · cited by 3sup_addIsLUB.add · cited by 2IsLUB.addinf_add · cited by 2inf_addcsInf_add · cited by 1csInf_addciSup_add · cited by 1ciSup_addsInf_add · cited by 1sInf_addsSup_add · cited by 1sSup_addciInf_add · cited by 1ciInf_addOrderIso.addRight_apply · cited by 1OrderIso.addRight_applyRootPairing.chainBotCoeff_of_add · cited by 1RootPairing.chainBotCoeff…partialSups_add_const · cited by 0partialSups_add_constFinset.sup'_add · cited by 0Finset.sup'_addOrderIso.addRight.congr_simp · cited by 0addRight.congr_simpOrderIso.addRight_symm · cited by 0OrderIso.addRight_symmEquiv · cited by 8337EquivAddGroup · cited by 4410AddGroupOrderIso · cited by 874OrderIsoAddRightMono · cited by 367AddRightMonoEquiv.addRight · cited by 30Equiv.addRightOrderIso.addRightCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by16

Results whose statement or proof uses this declaration.