lift_apply' — Mathlib

English

The value of lift k G A F on f is the sum over the support of f of coefficient times F a.

Русский

Значение lift k G A F на f равно сумме по опорe f: коэффициент умножается на F a.

LaTeX

$$lift_apply' (F : G →* A) (f : MonoidAlgebra k G) = lift k G A F f = f.sum fun a b => algebraMap k A b * F a$$

Lean4

theorem lift_apply' (F : G →* A) (f : MonoidAlgebra k G) : lift k G A F f = f.sum fun a b => algebraMap k A b * F a :=
  rfl

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