Linear Independence and Block Matrices

This file provides lemmas about linear independence in the context of block-like matrices.

theorem Disjoint.matrix_one_eq_fromBlocks_toMatrixUnionUnion {α : Type u_1} {R : Type u_2} [DecidableEq α] [Zero R] [One R] {Zₗ Zᵣ : Set α} [(a : α) → Decidable (a ∈ Zₗ)] [(a : α) → Decidable (a ∈ Zᵣ)] (hZZ : Zₗ ⫗ Zᵣ) : 1 = (⊞ 1 0 0 1).toMatrixUnionUnion

theorem Matrix.linearIndepOn_iff_fromCols_zero {α : Type u_1} {R : Type u_2} [Ring R] {X Y I : Set α} (A : Matrix (↑X) (↑Y) R) (hIX : I ∩ X ⊆ X) (Y₀ : Set α) : LinearIndepOn R A hIX.elem.range ↔ LinearIndepOn R (A ◫ 0) hIX.elem.range

theorem Matrix.linearIndepOn_iff_zero_fromCols {α : Type u_1} {R : Type u_2} [Ring R] {X Y I : Set α} (A : Matrix (↑X) (↑Y) R) (hIX : I ∩ X ⊆ X) (Y₀ : Set α) : LinearIndepOn R A hIX.elem.range ↔ LinearIndepOn R (0 ◫ A) hIX.elem.range

theorem linearIndepOn_toMatrixUnionUnion_elem_range_iff {α : Type u_1} {R : Type u_2} [Ring R] {Xₗ Yₗ Xᵣ Yᵣ I : Set α} [(a : α) → Decidable (a ∈ Xₗ)] [(a : α) → Decidable (a ∈ Yₗ)] [(a : α) → Decidable (a ∈ Xᵣ)] [(a : α) → Decidable (a ∈ Yᵣ)] (hXX : Xₗ ⫗ Xᵣ) (hYY : Yₗ ⫗ Yᵣ) (Aₗ : Matrix (↑Xₗ) (↑Yₗ) R) (Aᵣ : Matrix (↑Xᵣ) (↑Yᵣ) R) (hI : I ⊆ Xₗ ∪ Xᵣ) (hIXₗ : I ∩ Xₗ ⊆ Xₗ) (hIXᵣ : I ∩ Xᵣ ⊆ Xᵣ) : LinearIndepOn R (⊞ Aₗ 0 0 Aᵣ).toMatrixUnionUnion hI.elem.range ↔ LinearIndepOn R Aₗ hIXₗ.elem.range ∧ LinearIndepOn R Aᵣ hIXᵣ.elem.range