lift_apply_of

Mathlib.GroupTheory.Abelianization.Defs

URI: https://scilib.ai/kg/mathlib#Abelianization.lift_apply_of

English

For x ∈ G, lift f (of x) = f x, i.e., the lift respects the generator images.

Русский

Для x ∈ G, lift f (of x) = f x, то есть подъём сохраняет образы генераторов.

LaTeX

$$$$ \\mathrm{lift}(f)(\\mathrm{of}(x)) = f(x). $$$$

Lean4

@[simp]
theorem lift_apply_of (x : G) : lift f (of x) = f x :=
  rfl

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

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

Разделы

Аффилиация

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