Mathlib Map

Theorems · Definition · order theory

toLex

{α : Type u_1} → α ≃ Lex α

toLex is the identity function to the Lex of a type.

Defined in
Mathlib.Order.Lex
Cited by
195 results in Mathlib
Foundations
Depth 11 from the axioms, rests on 40 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Sum.inlₗ · cited by 18Sum.inlₗSum.inrₗ · cited by 18Sum.inrₗMvPowerSeries.lexOrder · cited by 14MvPowerSeries.lexOrderCardinal.mul_eq_self · cited by 13Cardinal.mul_eq_selfHahnEmbedding.Partial.eval · cited by 13Partial.evaltoLexMulEquiv · cited by 9toLexMulEquivMonovaryOn.sum_smul_comp_perm_le_sum_smul · cited by 7MonovaryOn.sum_smul_comp_…Prod.Lex.toLex_le_toLex · cited by 6Lex.toLex_le_toLexMvPowerSeries.coeff_eq_zero_of_lt_lexOrder · cited by 5MvPowerSeries.coeff_eq_ze…ofLex_toLex · cited by 5ofLex_toLexMonomialOrder.lex · cited by 5MonomialOrder.lexWithBot.orderIsoPUnitSumLex · cited by 4WithBot.orderIsoPUnitSumL…WithTop.orderIsoSumLexPUnit · cited by 4WithTop.orderIsoSumLexPUn…Prod.Lex.toLex_lt_toLex · cited by 4Lex.toLex_lt_toLextoLexAddEquiv · cited by 4toLexAddEquivEquiv · cited by 8337EquivLex · cited by 370LexEquiv.refl · cited by 274Equiv.refltoLexCITED BYCITES

Cites3

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

  • Equivstatement · cited by 8,337
  • Lexstatement · cited by 370
  • Equiv.reflproof · cited by 274

Cited by220

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 220.