ExponentExists — Mathlib

English

There exists a positive integer n such that g^n = 1 for all g in the monoid.

Русский

Существует положительное число n такое, что для всякого g в моноиде выполняется g^n = 1.

LaTeX

$$$\\exists n>0\\,\\forall g:G, g^n=1$$$

Lean4

/-- A predicate on a monoid saying that there is a positive integer `n` such that `g ^ n = 1`
for all `g`. -/
@[to_additive /-- A predicate on an additive monoid saying that there is a positive integer `n` such that
    `n • g = 0` for all `g`. -/
    ]
def ExponentExists :=
  ∃ n, 0 < n ∧ ∀ g : G, g ^ n = 1

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