blockDiagonal'_pow — Mathlib

English

The blockDiagonal' construction is injective: if blockDiagonal' M = blockDiagonal' N then M = N.

Русский

Конструкция blockDiagonal' инъективна: если blockDiagonal' M = blockDiagonal' N, то M = N.

LaTeX

$$$ \\mathrm{blockDiagonal}' M = \\mathrm{blockDiagonal}' N \\iff M = N $$$

Lean4

@[simp]
theorem blockDiagonal'_pow [∀ i, DecidableEq (m' i)] [Fintype o] [∀ i, Fintype (m' i)] [Semiring α]
    (M : ∀ i, Matrix (m' i) (m' i) α) (n : ℕ) : blockDiagonal' (M ^ n) = blockDiagonal' M ^ n :=
  map_pow (blockDiagonal'RingHom m' α) M n

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