toAddSubgroup'_closure — Mathlib

English

Equivalence between AddSubgroup closure and Subgroup closure via the inverse image under Multiplicative.ofAdd.

Русский

Эквивалентность между AddSubgroup.closure и Subgroup.closure через предобраз под Multiplicative.ofAdd.

LaTeX

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

Lean4

theorem toAddSubgroup'_closure {A : Type*} [AddGroup A] (S : Set (Multiplicative A)) :
    (closure S).toAddSubgroup' = AddSubgroup.closure (Multiplicative.ofAdd ⁻¹' S) :=
  le_antisymm (toAddSubgroup'.to_galoisConnection.l_le <| (closure_le _).mpr <| AddSubgroup.subset_closure (G := A))
    ((AddSubgroup.closure_le _).mpr <| Subgroup.subset_closure (G := Multiplicative A))

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