mem_pow — Mathlib

English

Let S be a subset of a monoid α and n a natural number. Then a belongs to S^n if and only if there exist elements a1, …, an in S such that a = a1 a2 … an.

Русский

Пусть S ⊆ α, где α — моноид, и n ∈ ℕ. Тогда a ∈ S^n тогда и только тогда, существует последовательность a1, …, an ∈ S такая, что a = a1 a2 … an.

LaTeX

$$$$ a \in S^n \iff \exists a_1, \dots, a_n \in S,\ a_1 a_2 \cdots a_n = a $$$$

Lean4

@[to_additive]
theorem mem_pow {a : α} {n : ℕ} : a ∈ s ^ n ↔ ∃ f : Fin n → s, (List.ofFn fun i ↦ (f i : α)).prod = a := by
  rw [← mem_prod_list_ofFn, List.ofFn_const, List.prod_replicate]

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