ofScalars_series_eq_iff — Mathlib

English

Let E be nontrivial. For two coefficient sequences c, c', the scalar series are equal if and only if the sequences are equal: ofScalars E c = ofScalars E c' ⇔ c = c'.

Русский

Пусть E не тривиален. Тогда для любых последовательностей коэффициентов c, c' выполняется: ofScalars E c = ofScalars E c' ⇔ c = c'.

LaTeX

$$$[Nontrivial\ E]\;\operatorname{ofScalars} E c = \operatorname{ofScalars} E c' \iff c=c'$$$

Lean4

@[simp]
theorem ofScalars_series_eq_iff [Nontrivial E] (c' : ℕ → 𝕜) : ofScalars E c = ofScalars E c' ↔ c = c' :=
  ⟨fun e => ofScalars_series_injective 𝕜 E e, _root_.congrArg _⟩

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