repr_symm_single — Mathlib

English

For any i and scalar c, b.repr^{-1}(δ_i c) = c · b_i.

Русский

Для любого i и скаляра c: b.repr^{-1}(δ_i c) = c · b_i.

LaTeX

$$$b.\mathrm{repr}^{-1}(\delta_i c) = c \cdot b_i$$$

Lean4

theorem repr_symm_single : b.repr.symm (Finsupp.single i c) = c • b i :=
  calc
    b.repr.symm (Finsupp.single i c) = b.repr.symm (c • Finsupp.single i (1 : R)) := by {
      rw [Finsupp.smul_single', mul_one]
    }
    _ = c • b i := by rw [LinearEquiv.map_smul, repr_symm_single_one]

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