fromEnd_apply_single_one — Mathlib

English

For any i, the image of the coordinate vector with a 1 at i and zeros elsewhere under fromEnd equals f(b_i).

Русский

Для каждого i выполняется fromEnd R b f (e_i) = f(b_i), где e_i — единичный вектор координат.

LaTeX

$$$\\mathrm{fromEnd}(R,b,f)(\\Pi\\text{single } i\,1) = f(b_i)$$$

Lean4

theorem fromEnd_apply_single_one [DecidableEq ι] (f : Module.End R M) (i : ι) :
    PiToModule.fromEnd R b f (Pi.single i 1) = f (b i) := by
  rw [PiToModule.fromEnd_apply, Fintype.linearCombination_apply_single, one_smul]

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