mk'_toAddSubmonoid — Mathlib

English

The additive submonoid underlying Subsemiring.mk' s sm hm sa ha is sa.

Русский

Аддитивный подмоноид, лежащий в основе Subsemiring.mk' s sm hm sa ha, равен sa.

LaTeX

$$(Subsemiring.mk' s sm hm sa ha).toAddSubmonoid = sa$$

Lean4

@[simp]
theorem mk'_toAddSubmonoid {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubmonoid R} (ha : ↑sa = s) :
    (Subsemiring.mk' s sm hm sa ha).toAddSubmonoid = sa :=
  SetLike.coe_injective ha.symm

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