Theorems · Theorem · order theory

LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex

∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedCommGroupWithZero α] [inst_1 : LinearOrderedCommGroupWithZero β]
  {m : α} {n : β} (hm : m ≠ 0) (hn : n ≠ 0),
  (LinearOrderedCommGroupWithZero.inl α β) m * (LinearOrderedCommGroupWithZero.inr α β) n =
    ↑(toLex (Units.mk0 m hm, Units.mk0 n hn))

Defined in

Mathlib.Algebra.Order.GroupWithZero.Lex

Cited by

0 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderedCommGroupWithZeroLinearOrderedCommGroupWithZero