pow_eq_one_iff' — Mathlib

English

If a ≠ 1, then a^n = 1 implies n = 0, in a torsion-free monoid.

Русский

Если a ≠ 1, то a^n = 1 тогда и только тогда, когда n = 0, в торсионно-свободном моноиде.

LaTeX

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

Lean4

@[to_additive]
theorem pow_eq_one_iff' (ha : a ≠ 1) : a ^ n = 1 ↔ n = 0 :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ by rw [h, pow_zero]⟩
  by_contra h'
  simpa [h] using (pow_left_injective h').ne ha

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