pow_mul_subgroupClosure — Mathlib

English

For any nonempty s, and any n ∈ N, s^n multiplied by closure s equals closure s.

Русский

Для любого непустого s и любого n∈N, s^n·closure(s) = closure(s).

LaTeX

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

Lean4

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

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