liftNCRingHom_single — Mathlib

English

For a basis element a ∈ G and a scalar b ∈ k, liftNCRingHom applied to the single element a contains the product f(b) · g(ofAdd a).

Русский

Для базисного элемента a ∈ G и скаляра b ∈ k отображение liftNCRingHom на единственном элементе даёт произведение f(b) · g(ofAdd a).

LaTeX

$$$ liftNCRingHom\; f\; g\; h\; (single\ a\ b) = f\ b \cdot g\ (\text{ofAdd } a) $$$

Lean4

@[simp]
theorem liftNCRingHom_single (f : k →+* R) (g : Multiplicative G →* R) (h_comm) (a : G) (b : k) :
    liftNCRingHom f g h_comm (single a b) = f b * g (.ofAdd a) :=
  liftNC_single _ _ _ _

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