inl_mul_inr_eq_coe_toLex — Mathlib

English

Let m ∈ α, n ∈ β with m ≠ 0 and n ≠ 0. Then the product of the left embedding of m and the right embedding of n equals the lexicographic embedding of the pair (Units.mk0 m hm, Units.mk0 n hn).

Русский

Пусть m ∈ α, n ∈ β и m ≠ 0, n ≠ 0. Тогда произведение встращения слева в m и вправо в n равно лексикографическому вложению пары (Units.mk0 m hm, Units.mk0 n hn).

LaTeX

$$$$ m \neq 0 \land n \neq 0 \Rightarrow inl(\alpha,\beta)\, m \cdot inr(\alpha,\beta)\, n = toLex(Units.mk0(m, hm), Units.mk0(n, hn)) $$$$

Lean4

theorem inl_mul_inr_eq_coe_toLex {m : α} {n : β} (hm : m ≠ 0) (hn : n ≠ 0) :
    inl α β m * inr α β n = toLex (Units.mk0 _ hm, Units.mk0 _ hn) := by
  rw [inl_eq_coe_inlₗ hm, inr_eq_coe_inrₗ hn, ← WithZero.coe_mul, OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex]

Похожие утверждения