norm_inv_eq — Mathlib

English

The norm is invariant under taking inverses: norm(x^{-1}) = norm(x).

Русский

Норма сохраняется при взятии обратного элемента: norm(x^{-1}) = norm(x).

LaTeX

$$$$\\forall {\\\\alpha} \\, [\\\\text{inst } \\\\DecidableEq \\\\alpha], \\\\forall x: FreeGroup(\\\\alpha),\\\\;\\\\; \\mathrm{norm}(x^{-1}) = \\mathrm{norm}(x).$$$$

Lean4

@[to_additive (attr := simp)]
theorem norm_inv_eq {x : FreeGroup α} : norm x⁻¹ = norm x := by simp only [norm, toWord_inv, invRev_length]

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