one_mul — Mathlib

English

Multiplication by the multiplicative unit 1 is the left identity on EReal: for every x in EReal, 1 * x = x.

Русский

Умножение на единицу слева даёт тождественный элемент: для любого x в EReal, 1 · x = x.

LaTeX

$$$\forall x\in \mathrm{EReal}, 1 \cdot x = x$$$

Lean4

protected theorem one_mul : ∀ x : EReal, 1 * x = x
  | ⊤ => if_pos one_pos
  | ⊥ => if_pos one_pos
  | (x : ℝ) => congr_arg Real.toEReal (one_mul x)

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