mk'_toSubsemigroup — Mathlib

English

The Subsemigroup component of the mk' construction equals sm.

Русский

Компонент Subsemigroup конструирования mk' равен sm.

LaTeX

$$$ (\text{NonUnitalSubring.mk'}\, s\ sm\ sa\ hm\ ha).toSubsemigroup = sm. $$$

Lean4

@[simp]
theorem mk'_toSubsemigroup {s : Set R} {sm : Subsemigroup R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) :
    (NonUnitalSubring.mk' s sm sa hm ha).toSubsemigroup = sm :=
  SetLike.coe_injective hm.symm

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