Mathlib Map

Theorems · Theorem · order theory

ofLex_smul

∀ {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : Lex α), ofLex (b • a) = b • ofLex a
Defined in
Mathlib.Algebra.Order.Group.Synonym
Cited by
3 results in Mathlib
Foundations
Depth 14 from the axioms · uses Quot.sound
Assumes
SMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

MvPolynomial.supDegree_esymmAlgHomMonomial · cited by 2MvPolynomial.supDegree_es…HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff_of_orderTop_ofLex · cited by 1HahnSeries.archimedeanCla…HahnEmbedding.Partial.truncLT_mem_range_extendFun · cited by 1Partial.truncLT_mem_range…DFunLike.coe · cited by 62936DFunLike.coeEquiv · cited by 8337EquivLex · cited by 370LexofLex · cited by 127ofLexofLex_smulCITED BYCITES

Cites4

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

  • DFunLike.coestatement · cited by 62,936
  • Equivstatement · cited by 8,337
  • Lexstatement and proof · cited by 370
  • ofLexstatement · cited by 127

Cited by3

Results whose statement or proof uses this declaration.