ofScalars_series_injective — Mathlib

English

For a nontrivial E, the map c ↦ ofScalars E c is injective, i.e., if ofScalars E c = ofScalars E c' then c = c'.

Русский

При ненулевом E отображение c ↦ ofScalars E c инъективно: если ofScalars E c = ofScalars E c', то c = c'.

LaTeX

$$$[Nontrivial\ E]\;\operatorname{Injective}(\lambda c,\operatorname{ofScalars} E c)$$$

Lean4

theorem ofScalars_series_injective [Nontrivial E] : Function.Injective (ofScalars E (𝕜 := 𝕜)) :=
  by
  intro _ _
  refine Function.mtr fun h ↦ ?_
  simp_rw [FormalMultilinearSeries.ext_iff, ofScalars, ContinuousMultilinearMap.ext_iff,
    ContinuousMultilinearMap.smul_apply]
  push_neg
  obtain ⟨n, hn⟩ := Function.ne_iff.1 h
  refine ⟨n, fun _ ↦ 1, ?_⟩
  simp only [mkPiAlgebraFin_apply, List.ofFn_const, List.prod_replicate, one_pow, ne_eq]
  exact (smul_left_injective 𝕜 one_ne_zero).ne hn

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