dual_lc — Mathlib

English

For h a DualBases, for any l and i, ε i (DualBases.lc e l) = l i; i.e., dual coefficients recover l.

Русский

Для h = DualBases, для любого l и i: ε_i(DualBases.lc e l) = l i.

LaTeX

$$$ ε_i\\big( DualBases.lc\\ e\\ l\\big) = l_i $$$

Lean4

theorem dual_lc (l : ι →₀ R) (i : ι) : ε i (DualBases.lc e l) = l i :=
  by
  rw [lc, map_finsuppSum, Finsupp.sum_eq_single i (g := fun a b ↦ (ε i) (b • e a))]
  · simp [h.eval_same, smul_eq_mul]
  · intro q _ q_ne
    simp [h.eval_of_ne q_ne.symm, smul_eq_mul]
  · simp

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