toSubmonoid' — Mathlib

English

For any set S in M, the toAddSubmonoid of the closure of S equals the closure of the additive preimage of S.

Русский

Для множества S в M, toAddSubmonoid замыкания S эквивалентно замыканию аддитивного предобраза S.

LaTeX

$$$ \mathrm{toAddSubmonoid}(\mathrm{closure}(S)) = \mathrm{closure}(\mathrm{Additive.toMul}^{-1} S) $$$

Lean4

/-- Additive submonoids of an additive monoid `Additive M` are isomorphic to submonoids of `M`. -/
abbrev toSubmonoid' : AddSubmonoid (Additive M) ≃o Submonoid M :=
  Submonoid.toAddSubmonoid.symm

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