lift_of'

Mathlib.Algebra.MonoidAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#AddMonoidAlgebra.lift_of'

English

For x in G, lift on of' x equals F(Multiplicative.ofAdd x).

Русский

Для любого x∈G подъем на of'(k,G,x) равен F(Multiplicative.ofAdd x).

LaTeX

$$$\\mathrm{lift}_{k,G,A}(F)(\\mathrm{of'}(k,G,x)) = F(\\mathrm{Multiplicative.ofAdd}(x)).$$$

Lean4

theorem lift_of' (F : Multiplicative G →* A) (x : G) : lift k G A F (of' k G x) = F (Multiplicative.ofAdd x) :=
  lift_of F x

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

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

Разделы

Аффилиация

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