blockDiagonal'_inj

Mathlib.Data.Matrix.Block

URI: https://scilib.ai/kg/mathlib#Matrix.blockDiagonal'_inj

← MathLib Explorer

English

BlockDiagonal' M = BlockDiagonal' N if and only if M = N.

Русский

blockDiagonal' M = blockDiagonal' N тогда и только тогда, когда M = N.

LaTeX

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

Lean4

@[simp]
theorem blockDiagonal'_inj [DecidableEq o] {M N : ∀ i, Matrix (m' i) (n' i) α} :
    blockDiagonal' M = blockDiagonal' N ↔ M = N :=
  blockDiagonal'_injective.eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru