piRing_symm_apply — Mathlib

English

The inverse of piRing applied to f and g is the sum ∑ i g i • f i.

Русский

Обратное piRing применяется к f, g и равно сумме ∑ i g i • f i.

LaTeX

$$$$ (\\pi\\text{Ring}\\;R\\;M\\;ι\\;S)^{\\!\\mathrm{symm}} f\\, g = \\sum_i g_i \\cdot f_i, $$$$

Lean4

@[simp]
theorem piRing_symm_apply (f : ι → M) (g : ι → R) : (piRing R M ι S).symm f g = ∑ i, g i • f i := by
  simp [piRing, LinearMap.lsum_apply]
    -- TODO additive version?

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