mem_closure_pair — Mathlib

English

For a commutative group C and elements x,y,z ∈ C, z is in the closure of {x,y} if and only if z can be expressed as x^m y^n with integers m,n.

Русский

Для коммутативной группы C и элементов x,y,z ∈ C, z ∈ closure({x,y}) тогда и только тогда, когда z = x^m y^n для некоторых целых m,n.

LaTeX

$$$ z \\in \\overline{\\{x,y\\}} \\;\\iff\\; \\exists m,n \\in \\mathbb{Z},\\ x^{m} y^{n} = z $$$

Lean4

@[to_additive]
theorem mem_closure_pair {x y z : C} : z ∈ closure ({ x, y } : Set C) ↔ ∃ m n : ℤ, x ^ m * y ^ n = z :=
  by
  rw [← Set.singleton_union, Subgroup.closure_union, mem_sup]
  simp_rw [mem_closure_singleton, exists_exists_eq_and]

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