coe_pointwise_smul — Mathlib

English

The evaluation map is compatible with pointwise scalar multiplication: the coefficient of f • g at a equals f(a) • g(a).

Русский

Оценочная карта совместима с точечным скалярным умножением: коэффициент (f • g) на a равен f(a) • g(a).

LaTeX

$$$\\big( f \\cdot g \\big)(a) = f(a) \\cdot g(a)$$$

Lean4

@[simp]
theorem coe_pointwise_smul [Semiring β] (f : α → β) (g : α →₀ β) : ⇑(f • g) = f • ⇑g :=
  rfl

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