ofScalars — Mathlib

English

For FormalMultilinearSeries of scalars, the nth coefficient vanishes iff the scalar c(n) is zero, i.e., ofScalars E c n = 0 ↔ c(n) = 0, provided E is nontrivial.

Русский

Для формальной многолинейной серии коэффициент $n$-й пары равен нулю тогда и только тогда, когда скалярный коэффициент $c(n)$ равен нулю (при ненулевом $E$).

LaTeX

$$$ofScalars\\, E\\, c\\, n = 0 \\iff c(n) = 0$$$

Lean4

/-- Formal power series of `∑ cᵢ • xⁱ` for some scalar field `𝕜` and ring algebra `E` -/
def ofScalars (c : ℕ → 𝕜) : FormalMultilinearSeries 𝕜 E E := fun n ↦ c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E

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