mem_closure_iff_of_fintype — Mathlib

English

Let s be a finite subset of a commutative group M, and x ∈ closure s. Then there exists a: s → ℤ with x = ∏ i : s, i.1^{a(i)}.

Русский

Пусть s — конечное подмножество группы M; если x ∈ closure s, то существует a: s → ℤ такое, что x = ∏ i : s, i.1^{a(i)}.

LaTeX

$$$x \in \overline{s} \iff \exists a: s \to \mathbb{Z},\; x = \prod_{i: s} i.1^{a(i)}$$$

Lean4

@[to_additive]
theorem mem_closure_iff_of_fintype {s : Set M} [Fintype s] : x ∈ closure s ↔ ∃ a : s → ℤ, x = ∏ i : s, i.1 ^ a i :=
  by
  conv_lhs => rw [← Subtype.range_coe (s := s)]
  exact mem_closure_range_iff_of_fintype

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