constFormalMultilinearSeries_apply_of_nonzero

English

If n ≠ 0, then the nth term of constFormalMultilinearSeries is zero.

Русский

Если n ≠ 0, то n-й член константной формальной серии равен нулю.

LaTeX

$$$ n \\neq 0 \\implies constFormalMultilinearSeries 𝕜 E c n = 0 $$$

Lean4

theorem constFormalMultilinearSeries_apply_of_nonzero [NontriviallyNormedField 𝕜] [NormedAddCommGroup E]
    [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {c : F} {n : ℕ} (hn : n ≠ 0) :
    constFormalMultilinearSeries 𝕜 E c n = 0 :=
  Nat.casesOn n (fun hn => (hn rfl).elim) (fun _ _ => rfl) hn

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