coe_normUnit — Mathlib

English

In a commutative group with zero, for a nonzero element a, the coe of its normUnit equals a^(-1).

Русский

В коммутативном групповом моноиде с нулём для не нулевого элемента a отображение нормализованной единицы равно a^(-1).

LaTeX

$$$$ \\text{coe}(\\text{normUnit}(a)) = a^{-1} \\quad \\text{for } a \\neq 0. $$$$

Lean4

@[simp]
theorem coe_normUnit {a : G₀} (h0 : a ≠ 0) : (↑(normUnit a) : G₀) = a⁻¹ := by simp [normUnit, h0]

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