def Matrix.IsSubsetReducible {ι : Type u_1} [Fintype ι] {R : Type u_2} [Zero R] (A : Matrix ι ι R) : Prop

Chapter01 Definition 1.2.11. A square matrix indexed by a finite type is subset reducible if there is a nonempty proper subset J of indices such that A k j = 0 for every k ∈ J and j ∉ J. For A : Matrix (Fin n) (Fin n) ℝ, this is exactly the source definition.

@[implicit_reducible]

noncomputable instance Matrix.instDecidableIsSubsetReducible {ι : Type u_1} [Fintype ι] {R : Type u_2} [Zero R] (A : Matrix ι ι R) : Decidable A.IsSubsetReducible

Source subset reducibility is classically decidable.

def Matrix.IsSubsetIrreducible {ι : Type u_1} [Fintype ι] {R : Type u_2} [Zero R] (A : Matrix ι ι R) : Prop

A square matrix is source-irreducible if it is not subset reducible.

@[simp]

theorem Matrix.isSubsetReducible_iff {ι : Type u_1} [Fintype ι] {R : Type u_2} [Zero R] (A : Matrix ι ι R) : A.IsSubsetReducible ↔ ∃ (J : Finset ι), J.Nonempty ∧ J.card < Fintype.card ι ∧ ∀ ⦃k j : ι⦄, k ∈ J → j ∉ J → A k j = 0

theorem Matrix.isSubsetReducible_iff_exists_blockTriangularForm {ι : Type u_1} [Fintype ι] [DecidableEq ι] {R : Type u_2} [Zero R] (A : Matrix ι ι R) : A.IsSubsetReducible ↔ ∃ (J : Finset ι), J.Nonempty ∧ J.card < Fintype.card ι ∧ have e := (Equiv.sumCompl fun (i : ι) => i ∉ J).symm; ((reindex e e) A).BlockTriangular (Sum.elim (fun (x : { a : ι // a ∉ J }) => 0) fun (x : { a : ι // ¬a ∉ J }) => 1)

The subset-reducibility condition is equivalent to a simultaneous row-column reindexing into a two-by-two block upper triangular form. The complement block is listed first so that the zero lower-left block matches the source vanishing condition A k j = 0 for k ∈ J and j ∉ J.

@[simp]

theorem Matrix.isSubsetIrreducible_iff_not_isSubsetReducible {ι : Type u_1} [Fintype ι] {R : Type u_2} [Zero R] (A : Matrix ι ι R) : A.IsSubsetIrreducible ↔ ¬A.IsSubsetReducible