mem_zpowers_iff — Mathlib

English

For any g ∈ G and h ∈ G, h ∈ zpowers(g) if and only if there exists an integer k with g^k = h.

Русский

Для любых g ∈ G и h ∈ G верно: h ∈ zpowers(g) тогда и только если существует целое k такое, что g^k = h.

LaTeX

$$$ h \in \operatorname{zpowers}(g) \iff \exists k \in \mathbb Z, g^k = h $$$

Lean4

@[to_additive]
theorem mem_zpowers_iff {g h : G} : h ∈ zpowers g ↔ ∃ k : ℤ, g ^ k = h :=
  Iff.rfl

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