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 _