toSubsemigroup — Mathlib

English

The closure of a Subsemigroup in Multiplicative A corresponds to AddSubsemigroup.closure under Preimage.

Русский

Замыкание подполугруппы в Multiplicative A соответствует AddSubsemigroup.closure через предобраз.

LaTeX

$$$\\text{Subsemigroup toAddSubsemigroup'}(\\text{Subsemigroup.closure } S) = \\text{AddSubsemigroup.closure}(\\text{Additive.ofMul}^{-1} S)$$$

Lean4

/-- Additive subsemigroups of an additive semigroup `A` are isomorphic to
multiplicative subsemigroups of `Multiplicative A`. -/
@[simps]
def toSubsemigroup : AddSubsemigroup A ≃o Subsemigroup (Multiplicative A)
    where
  toFun
    S :=
    { carrier := Multiplicative.toAdd ⁻¹' S
      mul_mem' := S.add_mem' }
  invFun
    S :=
    { carrier := Multiplicative.ofAdd ⁻¹' S
      add_mem' := S.mul_mem' }
  map_rel_iff' := Iff.rfl

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