pow_eq_one_iff — Mathlib

English

Let M be a monoid that is torsion-free with respect to multiplication. For any a ∈ M and any natural number n ≠ 0, a^n = 1 if and only if a = 1.

Русский

Пусть M — моноид, обладающий тождением без торсии: для любого a ∈ M и любого натурального n ≠ 0 верно a^n = 1 тогда и только тогда a = 1.

LaTeX

$$$ \\forall a \\in M, \\ \\forall n \\in \\mathbb{N},\\ n \\neq 0 \\Rightarrow (a^n = 1 \\iff a = 1).$$$

Lean4

@[to_additive]
theorem pow_eq_one_iff (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 :=
  ⟨fun h ↦ by rwa [← pow_left_inj hn, one_pow], fun h ↦ by rw [h, one_pow]⟩

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