English
The function sending a unit to its underlying value is injective: if u.val = v.val then u = v.
Русский
Функция, отправляющая единицу в её базовое значение, инъективна: если u.val = v.val, то u = v.
LaTeX
$$$$ u, v \\in \\alpha^{\\times}:\\ u .\\text{val} = v .\\text{val} \\Rightarrow u = v. $$$$
Lean4
@[to_additive]
theorem val_injective : Function.Injective (val : αˣ → α)
| ⟨v, i₁, vi₁, iv₁⟩, ⟨v', i₂, vi₂, iv₂⟩, e => by
simp only at e; subst v'; congr
simpa only [iv₂, vi₁, one_mul, mul_one] using mul_assoc i₂ v i₁