English
Let s be a family of bases for the coordinate spaces ιs j over Ms j. Then the basis element at index ji = (j,i) in the product space equals the function that is zero everywhere except at coordinate j, where it equals the i-th basis vector s_j i.
Русский
Пусть дана семейство базисов s_j для модулей M_j. Тогда базисный вектор, помеченный индексом ji = (j,i), в произведении равен функции, нулевой во всех координатах кроме координаты j, где он равен i-му базисному вектору s_j i.
LaTeX
$$$(\Pi\text{-basis } s)\ ji = \Pi\text{single } ji.1\ (s_{ji.1}\ ji.2)$$$
Lean4
@[simp]
theorem basis_apply [DecidableEq η] (s : ∀ j, Basis (ιs j) R (Ms j)) (ji) :
Pi.basis s ji = Pi.single ji.1 (s ji.1 ji.2) :=
Basis.apply_eq_iff.mpr (by simp)
