mul_left_inj — Mathlib

English

For any unitary U, right multiplication by U is injective: x · U = y · U implies x = y.

Русский

Для любого унитарного U правое умножение на U инъективно: x · U = y · U ⇒ x = y.

LaTeX

$$$ x U = y U \;\iff\; x = y \quad (\text{for all } x,y \in R) $$$

Lean4

/-- For unitary `U` in a star-monoid `R`, `x * U = y * U` if and only if `x = y`
for all `x` and `y` in `R`. -/
protected theorem mul_left_inj {x y : R} (U : unitary R) : x * U = y * U ↔ x = y :=
  unitary.val_toUnits_apply U ▸ Units.mul_left_inj _

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