English
BlockDiagonal extends to a ring homomorphism from o → Matrix m m α to Matrix (m × o) (m × o) α, respecting identity and multiplication.
Русский
BlockDiagonal допускает ринг-гомоморфизм от o → Matrix m m α к Matrix (m × o) (m × o) α, сохраняющий тождество и умножение.
LaTeX
$$$\text{BlockDiagonalRingHom} : (o \to Matrix\, m\, m\, α) \to_* (Matrix\, (m \times o) \, (m \times o) \, α)$$$
Lean4
/-- `Matrix.blockDiagonal` as a `RingHom`. -/
@[simps]
def blockDiagonalRingHom [DecidableEq m] [Fintype o] [Fintype m] [NonAssocSemiring α] :
(o → Matrix m m α) →+* Matrix (m × o) (m × o) α :=
{ blockDiagonalAddMonoidHom m m o α with
toFun := blockDiagonal
map_one' := blockDiagonal_one
map_mul' := blockDiagonal_mul }
