blockDiagonal'_apply_eq

Mathlib.Data.Matrix.Block

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

English

If k ≠ k', then blockDiagonal' M ⟨k,i⟩ ⟨k',j⟩ = 0.

Русский

Если k ≠ k', то blockDiagonal' M ⟨k,i⟩ ⟨k',j⟩ = 0.

LaTeX

$$$ blockDiagonal' M \langle k,i\rangle \langle k',j\rangle = 0 \quad \text{если } k \neq k' $$$

Lean4

@[simp]
theorem blockDiagonal'_apply_eq (M : ∀ i, Matrix (m' i) (n' i) α) (k i j) : blockDiagonal' M ⟨k, i⟩ ⟨k, j⟩ = M k i j :=
  dif_pos rfl

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

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

Разделы

Аффилиация

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