val_inv_eq_inv_val — Mathlib

English

For a unit u ∈ α^×, the underlying value of u^{-1} equals the inverse of the underlying value: ↑u^{-1} = (u)^{-1} in α.

Русский

Для единицы u ∈ α^× значение её обратного элемента подмножество в α равно обратному значению самой единицы.

LaTeX

$$$\uparrow(u^{-1}) = (u^{-1} : \alpha)$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem val_inv_eq_inv_val (u : αˣ) : ↑u⁻¹ = (u⁻¹ : α) :=
  Eq.symm <| inv_eq_of_mul_eq_one_right u.mul_inv

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