closure_toSubmonoid_of_finite — Mathlib

English

For a finite group G, the closure of a set s in Subgroup when mapped to Submonoid equals Submonoid.closure s.

Русский

Для конечной группы G замыкание множества s в Subgroup, отображаемое в Submonoid, совпадает с Submonoid.closure s.

LaTeX

$$Subgroup.closure_toSubmonoid_of_finite {s : Set G} : (closure s).toSubmonoid = Submonoid.closure s$$

Lean4

/-- See `Subgroup.closure_toSubmonoid_of_isOfFinOrder` for a version with weaker assumptions. -/
@[to_additive /-- See `AddSubgroup.closure_toAddSubmonoid_of_isOfFinOrder` for a version with weaker
    assumptions. -/
    ]
theorem closure_toSubmonoid_of_finite {s : Set G} : (closure s).toSubmonoid = Submonoid.closure s :=
  closure_toSubmonoid_of_isOfFinOrder <| by simp [isOfFinOrder_of_finite]

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