pi — Mathlib · SciLib

English

The nth coefficient of a scalar multiple a • f equals a times the nth coefficient of f.

Русский

Н-й коэффициент a • f равен a умноженному на n-й коэффициент f.

LaTeX

$$(a • f) n = a • f n$$

Lean4

/-- Product of formal multilinear series (with the same field `𝕜` and the same source
space, but possibly different target spaces). -/
@[simp]
def pi {ι : Type*} {F : ι → Type*} [∀ i, AddCommGroup (F i)] [∀ i, Module 𝕜 (F i)] [∀ i, TopologicalSpace (F i)]
    [∀ i, IsTopologicalAddGroup (F i)] [∀ i, ContinuousConstSMul 𝕜 (F i)] (p : Π i, FormalMultilinearSeries 𝕜 E (F i)) :
    FormalMultilinearSeries 𝕜 E (Π i, F i)
  | n => ContinuousMultilinearMap.pi (fun i ↦ p i n)

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