blockDiagonal'_injective

Mathlib.Data.Matrix.Block

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

← MathLib Explorer

English

BlockDiagonal' is injective: if blockDiagonal' M = blockDiagonal' N then M = N.

Русский

BlockDiagonal' инъективен: если blockDiagonal' M = blockDiagonal' N, то M = N.

LaTeX

$$$ \\text{Injective }( \\mathrm{blockDiagonal}' )$$

Lean4

theorem blockDiagonal'_injective [DecidableEq o] :
    Function.Injective (blockDiagonal' : (∀ i, Matrix (m' i) (n' i) α) → Matrix _ _ α) :=
  Function.LeftInverse.injective blockDiag'_blockDiagonal'

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

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

Разделы

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

Аффилиация

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