lc_coeffs — Mathlib

English

If two parameter families e and ε defining a DualBases are equal, then the resulting basis coincide; i.e., h.basis depends functorially on h.

Русский

Если два набора параметров e и ε, задающие DualBases, равны, то полученная база совпадает; то есть h.basis зависит по функции от h.

LaTeX

$$$ h.e = e' \\wedge h.\\epsilon = \\epsilon' \\Rightarrow h.basis = h'.basis $$$

Lean4

/-- For any m : M n, \sum_{p ∈ Q n} (ε p m) • e p = m -/
@[simp]
theorem lc_coeffs (m : M) : DualBases.lc e (h.coeffs m) = m :=
  h.total <| by simp [h.dual_lc]

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