toAddSubsemigroup' — Mathlib

English

The closure of a Subsemigroup under toAddSubsemigroup' equals the closure under the preimage via Additive.ofMul.

Русский

Замыкание подполугруппы под toAddSubsemigroup' совпадает с замыканием через предобраз Additive.ofMul.

LaTeX

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

Lean4

/-- Subsemigroups of a semigroup `Multiplicative A` are isomorphic to additive subsemigroups
of `A`. -/
abbrev toAddSubsemigroup' : Subsemigroup (Multiplicative A) ≃o AddSubsemigroup A :=
  AddSubsemigroup.toSubsemigroup.symm

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