English
There is an R-algebra structure on the matrix ring M_n(α) given by composing the algebra map R → α with the natural embedding α → M_n(α) via scalars.
Русский
Существует структура R-алгебры на кольце матриц M_n(α), задаваемая композицией алгебраического отображения R → α и естественным вложением α → M_n(α) через скаляры.
LaTeX
$$Algebra R (Matrix n n α) with algebraMap = (Matrix.scalar n) ∘ (algebraMap R α)$$
Lean4
instance instAlgebra : Algebra R (Matrix n n α)
where
algebraMap := (Matrix.scalar n).comp (algebraMap R α)
commutes' _ _ := scalar_commute _ (fun _ => Algebra.commutes _ _) _
smul_def' r x := by ext; simp [Matrix.scalar, Algebra.smul_def r]
