mul_subgroupClosure — Mathlib

English

If s is nonempty, then s multiplied by the closure of s equals the closure of s.

Русский

Если s непусто, то s умноженное на замыкание s равно замыканию s.

LaTeX

$$hs : s.Nonempty ⇒ s * closure s = closure s$$

Lean4

@[to_additive (attr := simp)]
theorem mul_subgroupClosure (hs : s.Nonempty) : s * closure s = closure s :=
  by
  rw [← smul_eq_mul, ← Set.iUnion_smul_set]
  have h a (ha : a ∈ s) : a • (closure s : Set G) = closure s := smul_coe_set <| subset_closure ha
  simp +contextual [h, hs]

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