one_mul — Mathlib

English

Multiplication by one on the left leaves a unchanged: 1 · a = a.

Русский

Умножение слева на единицу оставляет элемент без изменений: 1 · a = a.

LaTeX

$$$ 1 \cdot a = a $$$

Lean4

protected theorem one_mul (a : Nimber) : 1 * a = a :=
  by
  apply le_antisymm
  · refine mul_le_of_forall_ne fun x hx y hy ↦ ?_
    rw [Nimber.lt_one_iff_zero] at hx
    rw [hx, Nimber.one_mul, zero_mul, zero_mul, add_zero, zero_add]
    exact hy.ne
  · by_contra! h
    replace h := h
    exact (mul_left_cancel₀ one_ne_zero <| Nimber.one_mul _).not_lt h
termination_by a

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