norm_eq_zero — Mathlib

English

For any x in FreeGroup α, norm x = 0 if and only if x = 1.

Русский

Для любого x в FreeGroup α нормa x равна 0 тогда и только тогда, когда x = 1.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem norm_eq_zero {x : FreeGroup α} : norm x = 0 ↔ x = 1 := by
  simp only [norm, List.length_eq_zero_iff, toWord_eq_nil_iff]

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