subsemiringClosure_coe — Mathlib

English

The underlying set of the subsemiring closure of M equals the additive closure of M as a set: M.subsemiringClosure corresponds to AddSubmonoid.closure (M as a set).

Русский

Фактическое множество замыкания подsemiring ⟨M⟩ совпадает с аддитивным замыканием M как множества.

LaTeX

$$$(M.\\text{subsemiringClosure} : \\text{Set } R) = \\text{AddSubmonoid.closure} (M : \\text{Set } R)$$$

Lean4

theorem subsemiringClosure_coe : (M.subsemiringClosure : Set R) = AddSubmonoid.closure (M : Set R) :=
  rfl

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