range_subtype

Mathlib.Algebra.Group.Subgroup.Ker

URI: https://scilib.ai/kg/mathlib#Subgroup.range_subtype

← MathLib Explorer

English

Let H be a subgroup of G. Consider the inclusion map i from H into G. The image of this inclusion is exactly H.

Русский

Пусть H — подгруппа G. Пусть i: H → G — вложение. Его образ равен H.

LaTeX

$$$$ \\mathrm{Im}(i) = H $$$$

Lean4

@[to_additive (attr := simp)]
theorem _root_.Subgroup.range_subtype (H : Subgroup G) : H.subtype.range = H :=
  SetLike.coe_injective <| (coe_range _).trans <| Subtype.range_coe

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

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

Разделы

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

Аффилиация

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