Mathlib Map

Theorems · Definition · order theory

ofLexAddEquiv

(α : Type u_1) → [inst : Add α] → Lex α ≃+ α

ofLex as an AddEquiv.

Defined in
Mathlib.Algebra.Order.Group.Equiv
Cited by
4 results in Mathlib
Foundations
Depth 15 from the axioms · uses propext, Quot.sound
Assumes
Add
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ofLexLinearEquiv · cited by 3ofLexLinearEquivcoe_ofLexAddEquiv · cited by 0coe_ofLexAddEquivsymm_ofLexAddEquiv · cited by 0symm_ofLexAddEquivtoEquiv_ofLexAddEquiv · cited by 0toEquiv_ofLexAddEquivsymm_toLexAddEquiv · cited by 0symm_toLexAddEquivEquiv · cited by 8337EquivAddEquiv · cited by 1087AddEquivLex · cited by 370LexofLex · cited by 127ofLexofLexAddEquivCITED BYCITES

Cites4

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

  • Equivproof · cited by 8,337
  • AddEquivstatement · cited by 1,087
  • Lexstatement and proof · cited by 370
  • ofLexproof · cited by 127

Cited by5

Results whose statement or proof uses this declaration.