mk'_toAddSubgroup — Mathlib

English

The underlying additive subgroup of the subring Subring.mk' s sm sa hm ha is exactly sa.

Русский

Вложенное аддитивное подгрупповое множество подкольца Subring.mk' s sm sa hm ha равно sa.

LaTeX

$$$$(\mathrm{Subring.mk'}\ s\ sm\ sa\ hm\ ha).\mathrm{toAddSubgroup} = sa$$$$

Lean4

@[simp]
theorem mk'_toAddSubgroup {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) :
    (Subring.mk' s sm sa hm ha).toAddSubgroup = sa :=
  SetLike.coe_injective ha.symm

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