Mathlib Map

Theorems · Definition · order theory

ofLex

{α : Type u_1} → Lex α ≃ α

ofLex is the identity function from the Lex of a type.

Defined in
Mathlib.Order.Lex
Cited by
127 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.

Cardinal.mul_eq_self · cited by 13Cardinal.mul_eq_selfHahnEmbedding.Partial.evalCoeff · cited by 8Partial.evalCoeffHahnEmbedding.Partial.evalCoeff_eq · cited by 7Partial.evalCoeff_eqofLexMulEquiv · cited by 6ofLexMulEquivHahnSeries.lt_iff · cited by 5HahnSeries.lt_iffofLex_toLex · cited by 5ofLex_toLexofLexAddEquiv · cited by 4ofLexAddEquivOrderIso.sumLexCongr · cited by 4OrderIso.sumLexCongrHahnSeries.embDomainOrderEmbedding · cited by 4HahnSeries.embDomainOrder…HahnEmbedding.IsPartial.truncLT_mem_range · cited by 4IsPartial.truncLT_mem_ran…HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk · cited by 3Partial.orderTop_eq_archi…HahnEmbedding.Seed.coeff_baseEmbedding · cited by 3Seed.coeff_baseEmbeddingHahnSeries.orderTop_abs · cited by 3HahnSeries.orderTop_absProd.Lex.monotone_fst · cited by 3Lex.monotone_fstofLex_smul · cited by 3ofLex_smulEquiv · cited by 8337EquivLex · cited by 370LexEquiv.refl · cited by 274Equiv.reflofLexCITED 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 and proof · cited by 370
  • Equiv.reflproof · cited by 274

Cited by148

Results whose statement or proof uses this declaration.