mem_powers_iff — Mathlib

English

An element x lies in the submonoid generated by z iff there exists n ∈ ℕ with z^n = x.

Русский

Элемент x принадлежит подмоноиду порождаемому z тогда и только тогда, когда существует n ∈ ℕ с z^n = x.

LaTeX

$$$x \\in \\mathrm{powers}(z) \\\\iff \\\\exists n \\\\in \\\\mathbb{N}, z^n = x$$$

Lean4

theorem mem_powers_iff (x z : M) : x ∈ powers z ↔ ∃ n : ℕ, z ^ n = x :=
  Iff.rfl

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