unit_of_val_units — Mathlib

English

If a ∈ Units M corresponds to a unit in M, then the unit constructed from its value equals that unit.

Русский

Если a ∈ Units M соответствует единице в M, то единица, построенная из его значения, равна этой единице.

LaTeX

$$$\forall (a : Units\ M) (h : IsUnit a.val), IsUnit.unit from h = a$$$

Lean4

@[to_additive (attr := simp)]
theorem unit_of_val_units {a : Mˣ} (h : IsUnit (a : M)) : h.unit = a :=
  Units.ext rfl

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