exponent_eq_zero_iff_forall — Mathlib

English

Exponent(G) = 0 iff for every n > 0 there exists g ∈ G with g^n ≠ 1.

Русский

Exponent(G) = 0 тогда и только тогда, когда для каждого n>0 существует g ∈ G такой, что g^n ≠ 1.

LaTeX

$$$\\operatorname{exponent}(G) = 0 \\iff \\forall n>0, \\exists g:G, g^n \\neq 1$$$

Lean4

/-- The exponent is zero iff for all nonzero `n`, one can find a `g` such that `g ^ n ≠ 1`. -/
@[to_additive /-- The exponent is zero iff for all nonzero `n`, one can find a `g` such that
    `n • g ≠ 0`. -/
    ]
theorem exponent_eq_zero_iff_forall : exponent G = 0 ↔ ∀ n > 0, ∃ g : G, g ^ n ≠ 1 :=
  by
  rw [exponent_eq_zero_iff, ExponentExists]
  push_neg
  rfl

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