English
Two block matrices are equal iff all corresponding blocks are equal.
Русский
Два блочных матрицы равны тогда и только тогда, когда равны соответствующие блоки.
LaTeX
$$ext_iff_blocks {A B : Matrix (n ⊕ o) (l ⊕ m) α} : A = B ↔ A.toBlocks₁₁ = B.toBlocks₁₁ ∧ A.toBlocks₁₂ = B.toBlocks₁₂ ∧ A.toBlocks₂₁ = B.toBlocks₂₁ ∧ A.toBlocks₂₂ = B.toBlocks₂₂$$
Lean4
/-- Two block matrices are equal if their blocks are equal. -/
theorem ext_iff_blocks {A B : Matrix (n ⊕ o) (l ⊕ m) α} :
A = B ↔
A.toBlocks₁₁ = B.toBlocks₁₁ ∧
A.toBlocks₁₂ = B.toBlocks₁₂ ∧ A.toBlocks₂₁ = B.toBlocks₂₁ ∧ A.toBlocks₂₂ = B.toBlocks₂₂ :=
⟨fun h => h ▸ ⟨rfl, rfl, rfl, rfl⟩, fun ⟨h₁₁, h₁₂, h₂₁, h₂₂⟩ => by
rw [← fromBlocks_toBlocks A, ← fromBlocks_toBlocks B, h₁₁, h₁₂, h₂₁, h₂₂]⟩
