English
Let G be a group and S a subset of the additive structure on G. The closure of S inside the additive subgroup, transported back to the multiplicative subgroup, coincides with the closure of the preimage of S under Additive.ofMul.
Русский
Пусть G — группа, и S — подмножество аддитивной структуры над G. Замыкание S внутри аддитивной подгруппы, переносимое в мультипликативную подгруппу, совпадает с замыканием предобраза S под Additive.ofMul.
LaTeX
$$$ (AddSubgroup.closure S).toSubgroup' = Subgroup.closure (Additive.ofMul \\circ^{-1} S) $$$
Lean4
theorem _root_.AddSubgroup.toSubgroup'_closure (S : Set (Additive G)) :
(AddSubgroup.closure S).toSubgroup' = Subgroup.closure (Additive.ofMul ⁻¹' S) :=
congr_arg AddSubgroup.toSubgroup' (toAddSubgroup'_closure _).symm
