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 _