mul_one — Mathlib

English

The multiplication by 1 acts as the identity: (x) · 1 = x for all x in the Ore localization.

Русский

Умножение на единицу является тождественным: x · 1 = x для всех x в локализации Оре.

LaTeX

$$$ x \cdot 1 = x $$$

Lean4

@[to_additive]
protected theorem mul_one (x : R[S⁻¹]) : x * 1 = x :=
  by
  cases x with
  | _ r s
  simp [OreLocalization.one_def, oreDiv_mul_char r (1 : R) s (1 : S) r 1 (by simp)]

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