ofScalars_series_eq_zero — Mathlib

English

For any nontrivial target space E, the entire scalar formal multilinear series is zero if and only if the coefficient sequence c is identically zero: ofScalars E c = 0 ⇔ c = 0.

Русский

Пусть E не тривиально. Тогда вся скалярная формальная многочленная последовательность равна нулю тогда и только тогда, когда последовательность коэффициентов c идентично нулева.

LaTeX

$$$\operatorname{ofScalars} E c = 0 \iff c = 0$$$

Lean4

@[simp]
theorem ofScalars_series_eq_zero [Nontrivial E] : ofScalars E c = 0 ↔ c = 0 := by
  simp [FormalMultilinearSeries.ext_iff, funext_iff]

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