toSubgroup_closure — Mathlib

English

The closure in the additive world of the multiplicative image corresponds to AddSubgroup closure of the preimage under Multiplicative.ofAdd.

Русский

Замыкание в аддитивной вселенной образа через Multiplicative.ofAdd соответствует AddSubgroup.closure предобразу.

LaTeX

$$$ (\mathrm{closure} S).\mathrm{toAddSubgroup'} = \mathrm{AddSubgroup.closure}(\mathrm{Multiplicative.ofAdd}^{-1} S) $$$

Lean4

theorem _root_.AddSubgroup.toSubgroup_closure {A : Type*} [AddGroup A] (S : Set A) :
    (AddSubgroup.closure S).toSubgroup = Subgroup.closure (Multiplicative.toAdd ⁻¹' S) :=
  Subgroup.toAddSubgroup.injective (Subgroup.toAddSubgroup_closure _).symm

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