English
For any index i of the sum ι ⊕ ι', the product basis applied to i equals the appropriate left or right embedding of the corresponding basis.
Русский
Для любого индекса i из суммирования ι ⊕ ι' базис произведения применён к i даёт либо соответствующее левое внедрение базиса, либо правое.
LaTeX
$$b.prod b' i = \mathrm{Sum.elim} (\mathrm{LinearMap.inl} R M M' \circ b) (\mathrm{LinearMap.inr} R M M' \circ b') i$$
Lean4
@[simp]
theorem prod_apply (i) : b.prod b' i = Sum.elim (LinearMap.inl R M M' ∘ b) (LinearMap.inr R M M' ∘ b') i := by
ext <;> cases i <;>
simp only [prod_apply_inl_fst, Sum.elim_inl, LinearMap.inl_apply, prod_apply_inr_fst, Sum.elim_inr,
LinearMap.inr_apply, prod_apply_inl_snd, prod_apply_inr_snd, Function.comp]
