liftNCRingHom_single — Mathlib

English

On a basis element, liftNCRingHom evaluates to the product of the base-ring image of the coefficient and the monoid-homomorphism image of the group element.

Русский

На базисном элементе liftNCRingHom расчитывается как произведение образа коэффициента в кольцо основы и образа моноидного отображения группы элемента.

LaTeX

$$$liftNCRingHom\ f\ g (single a b) = f(b) \cdot g(a)$$$

Lean4

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

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