mk'_toSubmonoid — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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