mul_right_inj — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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