linearEquivFunOnFintype_symm_single

English

The inverse sends Pi.single i m to lof i m.

Русский

Обратное отображение переводит Pi.single i m в lof i m.

LaTeX

$$$ (linearEquivFunOnFintype\\; R\\; ι\\; M)^{\\mathrm{symm}} (\\mathrm{Pi.single}\\; i\\; m) = \\mathrm{lof}\\; R\\; ι\\; M\\; i\\; m $$$

Lean4

@[simp]
theorem linearEquivFunOnFintype_symm_single [Fintype ι] (i : ι) (m : M i) :
    (linearEquivFunOnFintype R ι M).symm (Pi.single i m) = lof R ι M i m :=
  DFinsupp.equivFunOnFintype_symm_single i m

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