mk'_toAddSubgroup

Mathlib.RingTheory.NonUnitalSubring.Defs

URI: https://scilib.ai/kg/mathlib#NonUnitalSubring.mk'_toAddSubgroup

← MathLib Explorer

English

The AddSubgroup component of the mk' construction equals sa.

Русский

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

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru