linearEquivFunOnFintype_lof — Mathlib

English

The linear equivalence sends lof R ι M i m to Pi.single i m.

Русский

Линейное эквивалентное отображение переводит lof R ι M i m в Pi.single i m.

LaTeX

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

Lean4

@[simp]
theorem linearEquivFunOnFintype_lof [Fintype ι] (i : ι) (m : M i) :
    (linearEquivFunOnFintype R ι M) (lof R ι M i m) = Pi.single i m := by rfl

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