ofScalars_eq_zero_of_scalar_zero — Mathlib

English

Let c: N → 𝕜 be a sequence. If the n-th coefficient vanishes, i.e. c(n) = 0, then the corresponding nth coefficient of the scalar formal multilinear series is zero: for every n, c(n) = 0 implies ofScalars E c n = 0.

Русский

Пусть c: ℕ → 𝕜. Если n-й коэффициент обращается в ноль, то соответствующий n-й член скалярной формальной многочленной последовательности равен нулю: для всякого n верно, что c(n) = 0 ⇒ ofScalars E c n = 0.

LaTeX

$$$\forall n \in \mathbb{N},\ c(n)=0 \Rightarrow \operatorname{ofScalars} E c n = 0$$$

Lean4

@[simp]
theorem ofScalars_eq_zero_of_scalar_zero {n : ℕ} (hc : c n = 0) : ofScalars E c n = 0 := by
  rw [ofScalars, hc, zero_smul 𝕜 (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)]

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