pow_eq_one_iff — Mathlib

English

Let M be a monoid with a linear order compatible with multiplication, and with left-multiplication monotone. Then for every x ∈ M and every n ∈ ℕ with n ≠ 0, x^n = 1 if and only if x = 1.

Русский

Пусть M — моноид с линейным порядком, совместимым с умножением, и левая монотонность умножения. Тогда для любого x ∈ M и любого n ∈ ℕ, такого что n ≠ 0, верно x^n = 1 тогда и только тогда, когда x = 1.

LaTeX

$$$\forall x \in M, \forall n \in \mathbb{N}, n \neq 0 \Rightarrow x^n = 1 \iff x = 1$$$

Lean4

@[to_additive]
theorem pow_eq_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n = 1 ↔ x = 1 :=
  by
  simp only [le_antisymm_iff]
  rw [pow_le_one_iff hn, one_le_pow_iff hn]

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