blockDiagonal'RingHom — Mathlib

English

BlockDiagonal' commutes with natural powers: blockDiagonal'(M^n) = (blockDiagonal' M)^n.

Русский

BlockDiagonal' коммутирует с натуральными степенями: blockDiagonal'(M^n) = (blockDiagonal' M)^n.

LaTeX

$$$ \\mathrm{blockDiagonal}'(M^{n}) = (\\mathrm{blockDiagonal}' M)^{n} $$$

Lean4

/-- `Matrix.blockDiagonal'` as a `RingHom`. -/
@[simps]
def blockDiagonal'RingHom [∀ i, DecidableEq (m' i)] [Fintype o] [∀ i, Fintype (m' i)] [NonAssocSemiring α] :
    (∀ i, Matrix (m' i) (m' i) α) →+* Matrix (Σ i, m' i) (Σ i, m' i) α :=
  { blockDiagonal'AddMonoidHom m' m' α with
    toFun := blockDiagonal'
    map_one' := blockDiagonal'_one
    map_mul' := blockDiagonal'_mul }

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