range_mk'

Mathlib.GroupTheory.QuotientGroup.Defs

URI: https://scilib.ai/kg/mathlib#QuotientGroup.range_mk'

English

The range of the quotient map mk' is the top subgroup; i.e., mk' is surjective onto the quotient.

Русский

Образ отображения mk' равен верхнему подгруппе; то есть mk' сюръективна на фактор-группу.

LaTeX

$$$\\text{range} (\\text{mk}' \\ N) = \\top$$$

Lean4

@[to_additive (attr := simp)]
theorem range_mk' : (QuotientGroup.mk' N).range = ⊤ :=
  MonoidHom.range_eq_top.mpr (mk'_surjective N)

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

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

Разделы

Аффилиация

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