lift_single — Mathlib

English

For a multiplicative G →* A and a,b in the ground rings, lift evaluated at the basis element single a b equals b times F(Multiplicative.ofAdd a).

Русский

Для отображения F: Multiplicative G →* A и элементов a∈G, b∈k верно: lift(k,G,A,F)(single a b) = b · F(Multiplicative.ofAdd a).

LaTeX

$$$\\mathrm{lift}_{k,G,A}(F)(\\mathrm{single}(a,b)) = b \\cdot F(\\mathrm{Multiplicative.ofAdd}(a)).$$$

Lean4

@[simp]
theorem lift_single (F : Multiplicative G →* A) (a b) : lift k G A F (single a b) = b • F (Multiplicative.ofAdd a) :=
  MonoidAlgebra.lift_single F (.ofAdd a) b

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