Mathlib Map

Theorems · Definition · order theory

toLexMulEquiv

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

toLex as a MulEquiv.

Defined in
Mathlib.Algebra.Order.Group.Equiv
Cited by
9 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.inl · cited by 4LinearOrderedCommGroupWit…LinearOrderedCommGroupWithZero.inr · cited by 3LinearOrderedCommGroupWit…LinearOrderedCommGroupWithZero.fst · cited by 2LinearOrderedCommGroupWit…LinearOrderedCommGroupWithZero.inl_apply · cited by 2LinearOrderedCommGroupWit…LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ · cited by 1LinearOrderedCommGroupWit…LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ · cited by 1LinearOrderedCommGroupWit…LinearOrderedCommGroupWithZero.inr_apply · cited by 1LinearOrderedCommGroupWit…toEquiv_toLexMulEquiv · cited by 0toEquiv_toLexMulEquivLinearOrderedCommGroupWithZero.fst_comp_inl · cited by 0LinearOrderedCommGroupWit…symm_ofLexMulEquiv · cited by 0symm_ofLexMulEquivcoe_toLexMulEquiv · cited by 0coe_toLexMulEquivsymm_toLexMulEquiv · cited by 0symm_toLexMulEquivEquiv · cited by 8337EquivMulEquiv · cited by 1142MulEquivLex · cited by 370LextoLex · cited by 195toLextoLexMulEquivCITED 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
  • toLexproof · cited by 195

Cited by12

Results whose statement or proof uses this declaration.