rangeRestrict_surjective

Mathlib.Algebra.Group.Subgroup.Ker

URI: https://scilib.ai/kg/mathlib#MonoidHom.rangeRestrict_surjective

English

For a monoid hom f: G →* N, range equals top subgroup of N if and only if f is surjective.

Русский

Образ f равен верхней подгруппе если и только если f сюръективен.

LaTeX

$$f.range = \top \Leftrightarrow Function.Surjective(f)$$

Lean4

@[to_additive]
theorem rangeRestrict_surjective (f : G →* N) : Function.Surjective f.rangeRestrict := fun ⟨_, g, rfl⟩ => ⟨g, rfl⟩

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

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

Разделы

Аффилиация

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