Mathlib Map

Theorems · Definition · order theory

ofLexMulEquiv

(α : Type u_1) → [inst : Mul α] → Lex α ≃* α

ofLex as a MulEquiv.

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

Around this declaration

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

LinearOrderedCommGroupWithZero.fst_apply · cited by 1LinearOrderedCommGroupWit…LinearOrderedCommGroupWithZero.fst_comp_inl · cited by 0LinearOrderedCommGroupWit…coe_ofLexMulEquiv · cited by 0coe_ofLexMulEquivsymm_ofLexMulEquiv · cited by 0symm_ofLexMulEquivtoEquiv_ofLexMulEquiv · cited by 0toEquiv_ofLexMulEquivsymm_toLexMulEquiv · cited by 0symm_toLexMulEquivEquiv · cited by 8337EquivMulEquiv · cited by 1142MulEquivLex · cited by 370LexofLex · cited by 127ofLexofLexMulEquivCITED 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
  • MulEquivstatement · cited by 1,142
  • Lexstatement and proof · cited by 370
  • ofLexproof · cited by 127

Cited by6

Results whose statement or proof uses this declaration.