subst_mul — Mathlib

English

The set of indices contributing to the substituted coefficient is finite: for each a, f, e, the set {d | coeff d f • coeff e (a^d)} is finite.

Русский

Множество индексов, вносящих вклад в подстановочный коэффициент, конечно: для любых f,e,a множество {d | коэффициент d f · коэффициент e (a^d)} конечно.

LaTeX

$$$\\forall ha\\, (f : PowerSeries R)\\, (e : Finsupp\\;\\tau\\;\\mathbb{N}), \\\\ Finite\\left(\\{ d \\mid coeff\\; d\\, f \\cdot coeff\\; e (a^d) \}\\right)$$$

Lean4

theorem subst_mul (ha : HasSubst a) (f g : PowerSeries R) : subst a (f * g) = subst a f * subst a g := by
  rw [← coe_substAlgHom ha, map_mul]

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