toSubsemigroup' — Mathlib

English

AddSubsemigroups of an additive semigroup are isomorphic to Subsemigroups of the corresponding Multiplicative A.

Русский

Аддитивные подполугруппы аддитивного полугруппы эквивалентны подполугруппам соответствующей мультипликативной структуры.

LaTeX

$$$\\text{AddSubsemigroup } A \\simeq_o \\text{Subsemigroup}(\\text{Multiplicative } A)$$$

Lean4

/-- Additive subsemigroups of an additive semigroup `Additive M` are isomorphic to subsemigroups
of `M`. -/
abbrev toSubsemigroup' : AddSubsemigroup (Additive M) ≃o Subsemigroup M :=
  Subsemigroup.toAddSubsemigroup.symm

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