subgroupClosure_mul_pow — Mathlib

English

For a nonempty set s and any n, the product of the closure of s with the nth power of s equals the closure of s.

Русский

Для непустого s и любого n, произведение замыкания s и n-й степени s равно замыканию s.

LaTeX

$$hs : s.Nonempty ⇒ ∀ n, closure s * (s ^ n) = closure s$$

Lean4

@[to_additive (attr := simp)]
theorem subgroupClosure_mul_pow (hs : s.Nonempty) : ∀ n, closure s * s ^ n = closure s
  | 0 => by simp
  | n + 1 => by rw [pow_succ', ← mul_assoc, subgroupClosure_mul hs, subgroupClosure_mul_pow hs]

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