English
There is a natural algebra hom structure on the product of endomorphism rings given by prodMap; this defines a map from End_R(M) × End_R(M₂) to End_R(M × M₂) that preserves addition and multiplication.
Русский
Существует естественная алгебра-гомоморфная структура на произведении концевых отображений заданная prodMap; она задает отображение End_R(M) × End_R(M₂) → End_R(M × M₂), сохраняющее сложение и умножение.
LaTeX
$$$ \\text{prodMapAlgHom} : (End_R M \\times End_R M_2) \\to_{\\!a[R]} End_R(M \\times M_2) $$$
Lean4
theorem inl_map_mul (a₁ a₂ : A) : LinearMap.inl R A B (a₁ * a₂) = LinearMap.inl R A B a₁ * LinearMap.inl R A B a₂ :=
Prod.ext rfl (by simp)
