val_injective — Mathlib

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₁

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