ext_hom

Mathlib.GroupTheory.FreeGroup.IsFreeGroup

URI: https://scilib.ai/kg/mathlib#IsFreeGroup.ext_hom

English

A variant of ext_hom: equality of MonoidHom on generators implies equality.

Русский

Вариант ext_hom: равенство MonoidHom на генераторах влечёт равенство.

LaTeX

$$∃ h : ∀ i, f(b(i)) = g(b(i)) → f = g$$

Lean4

theorem ext_hom ⦃f g : G →* H⦄ (h : ∀ a : Generators G, f (of a) = g (of a)) : f = g :=
  lift.symm.injective (funext h)

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

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

Разделы

Аффилиация

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