algebraMap_eq_diagonalRingHom — Mathlib

English

The algebra map R → Matrix n n α factors as the composition of the diagonalRingHom from (n → α) to Matrix n n α with the algebra map R → (n → α).

Русский

Общее отображение R → Matrix n n α разлагается как композиция диагонального кольца (диагональное отображение) из n→α в Matrix n n α и алгебраического отображения R → (n→α).

LaTeX

$$algebraMap R (Matrix n n α) = (Matrix.diagonalRingHom n α) ∘ (algebraMap R (n → α))$$

Lean4

theorem algebraMap_eq_diagonalRingHom : algebraMap R (Matrix n n α) = (diagonalRingHom n α).comp (algebraMap R _) :=
  rfl

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