lift_symm_apply

Mathlib.GroupTheory.FreeGroup.IsFreeGroup

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

English

If homomorphisms are equal on all generators, they are equal.

Русский

Если гомоморфизмы равны на всех генераторах, они равны.

LaTeX

$$∃ i, f(b(i)) = g(b(i)) ⇒ f = g$$

Lean4

@[simp]
theorem lift_symm_apply (f : G →* H) (a : Generators G) : (lift.symm f) a = f (of a) :=
  rfl

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

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

Разделы

Аффилиация

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