toAddSubmonoid — Mathlib

English

The map from a subalgebra to its additive submonoid is defined.

Русский

Определено отображение подпалгебры в её аддитивную подмоноиду.

LaTeX

$$$$ \\text{toAddSubmonoid}(S) = \\text{AddSubmonoid}(A)\\text{ derived from } S $$$$

Lean4

/-- The projection from a subalgebra of `A` to an additive submonoid of `A`. -/
@[simps coe]
def toAddSubmonoid {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) :
    AddSubmonoid A :=
  S.toSubsemiring.toAddSubmonoid

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