This file provides notation used in the project and conversions between set-theoretical and type-theoretical definitions.

@[reducible, inline]

abbrev Z2 : Type

The finite field on 2 elements; write Z2 for "value" type but Fin 2 for "indexing" type.

Equations

• Z2 = ZMod 2

@[reducible, inline]

abbrev Z3 : Type

The finite field on 3 elements; write Z3 for "value" type but Fin 3 for "indexing" type.

Equations

• Z3 = ZMod 3

def «term_ᕃ_» : Lean.TrailingParserDescr

Roughly speaking a ᕃ A is A ∪ {a}.

Equations

• «term_ᕃ_» = Lean.ParserDescr.trailingNode `«term_ᕃ_» 66 67 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ᕃ ") (Lean.ParserDescr.cat `term 66))

def «term_⫗_» : Lean.TrailingParserDescr

Writing X ⫗ Y is slightly more general than writing X ∩ Y = ∅.

Equations

• «term_⫗_» = Lean.ParserDescr.trailingNode `«term_⫗_» 61 62 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⫗ ") (Lean.ParserDescr.cat `term 62))

def «term_.→» : Lean.TrailingParserDescr

The left-to-right direction of ↔.

Equations

• «term_.→» = Lean.ParserDescr.trailingNode `«term_.→» 1024 1024 (Lean.ParserDescr.symbol ".→")

def «term_.←» : Lean.TrailingParserDescr

The right-to-left direction of ↔.

Equations

• «term_.←» = Lean.ParserDescr.trailingNode `«term_.←» 1024 1024 (Lean.ParserDescr.symbol ".←")

theorem Fin2_eq_1_of_ne_0 {a : Fin 2} (ha : a ≠ 0) : a = 1

theorem Fin3_eq_2_of_ne_0_1 {a : Fin 3} (ha0 : a ≠ 0) (ha1 : a ≠ 1) : a = 2

theorem Z2val_toRat_mul_Z2val_toRat (a b : Z2) : ↑(ZMod.val a) * ↑(ZMod.val b) = ↑(ZMod.val (a * b))

@[reducible, inline]

abbrev Matrix.prependId {α : Type} [Zero α] [One α] {m n : Type} [DecidableEq m] [DecidableEq n] (A : Matrix m n α) : Matrix m (m ⊕ n) α

Equations

• A.prependId = Matrix.fromCols 1 A

theorem Matrix.det_coe {α : Type} [DecidableEq α] [Fintype α] (A : Matrix α α ℤ) (F : Type) [Field F] : ↑A.det = (A.map Int.cast).det

theorem IsUnit.linearIndependent_matrix {α : Type} [DecidableEq α] [Fintype α] {R : Type} [CommRing R] {A : Matrix α α R} (hA : IsUnit A) : LinearIndependent R A

def HasSubset.Subset.elem {α : Type} {X Y : Set α} (hXY : X ⊆ Y) (x : ↑X) : ↑Y

Given X ⊆ Y cast an element of X as an element of Y.

Equations

• hXY.elem x = ⟨↑x, ⋯⟩

theorem HasSubset.Subset.elem_injective {α : Type} {X Y : Set α} (hXY : X ⊆ Y) : Function.Injective hXY.elem

def Subtype.toSum {α : Type} {X Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] (i : ↑(X ∪ Y)) : ↑X ⊕ ↑Y

Convert (X ∪ Y).Elem to X.Elem ⊕ Y.Elem.

Equations

• Subtype.toSum i = if hiX : ↑i ∈ X then Sum.inl ⟨↑i, hiX⟩ else if hiY : ↑i ∈ Y then Sum.inr ⟨↑i, hiY⟩ else ⋯.elim

def Sum.toUnion {α : Type} {X Y : Set α} (i : ↑X ⊕ ↑Y) : ↑(X ∪ Y)

Convert X.Elem ⊕ Y.Elem to (X ∪ Y).Elem.

Equations

• i.toUnion = Sum.casesOn i ⋯.elem ⋯.elem

theorem toSum_toUnion {α : Type} {X Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] (i : ↑(X ∪ Y)) : (Subtype.toSum i).toUnion = i

Converting (X ∪ Y).Elem to X.Elem ⊕ Y.Elem and back to (X ∪ Y).Elem gives the original element.

theorem toUnion_toSum {α : Type} {X Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] (hXY : X ⫗ Y) (i : ↑X ⊕ ↑Y) : Subtype.toSum i.toUnion = i

Converting X.Elem ⊕ Y.Elem to (X ∪ Y).Elem and back to X.Elem ⊕ Y.Elem gives the original element, assuming that X and Y are disjoint.

def Matrix.toMatrixUnionUnion {α : Type} {T₁ T₂ S₁ S₂ : Set α} {β : Type} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(a : α) → Decidable (a ∈ S₁)] [(a : α) → Decidable (a ∈ S₂)] (C : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) β) : Matrix (↑(T₁ ∪ T₂)) (↑(S₁ ∪ S₂)) β

Convert a block matrix to a matrix over set unions.

Equations

• C.toMatrixUnionUnion x✝ = (C ∘ Subtype.toSum) x✝ ∘ Subtype.toSum

def Matrix.toMatrixSumSum {α : Type} {T₁ T₂ S₁ S₂ : Set α} {β : Type} (C : Matrix (↑(T₁ ∪ T₂)) (↑(S₁ ∪ S₂)) β) : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) β

Convert a matrix over set unions to a block matrix.

Equations

• C.toMatrixSumSum x✝ = (C ∘ Sum.toUnion) x✝ ∘ Sum.toUnion

theorem toMatrixUnionUnion_toMatrixSumSum {α : Type} {T₁ T₂ S₁ S₂ : Set α} {β : Type} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(a : α) → Decidable (a ∈ S₁)] [(a : α) → Decidable (a ∈ S₂)] (hT : T₁ ⫗ T₂) (hS : S₁ ⫗ S₂) (C : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) β) : C.toMatrixUnionUnion.toMatrixSumSum = C

Converting a block matrix to a matrix over set unions and back to a block matrix gives the original matrix, assuming that both said unions are disjoint.

theorem toMatrixSumSum_toMatrixUnionUnion {α : Type} {T₁ T₂ S₁ S₂ : Set α} {β : Type} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(a : α) → Decidable (a ∈ S₁)] [(a : α) → Decidable (a ∈ S₂)] (C : Matrix (↑(T₁ ∪ T₂)) (↑(S₁ ∪ S₂)) β) : C.toMatrixSumSum.toMatrixUnionUnion = C

Converting a matrix over set unions to a block matrix and back to a matrix over set unions gives the original matrix.

theorem Matrix.IsTotallyUnimodular.toMatrixUnionUnion {α : Type} {T₁ T₂ S₁ S₂ : Set α} {β : Type} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(a : α) → Decidable (a ∈ S₁)] [(a : α) → Decidable (a ∈ S₂)] [CommRing β] {C : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) β} (hC : C.IsTotallyUnimodular) : C.toMatrixUnionUnion.IsTotallyUnimodular

A totally unimodular block matrix stays totally unimodular after converting to a matrix over set unions.

theorem Matrix.overZ2_isTotallyUnimodular {X Y : Type} (A : Matrix X Y Z2) : A.IsTotallyUnimodular

theorem Matrix.overZ3_isTotallyUnimodular {X Y : Type} (A : Matrix X Y Z3) : A.IsTotallyUnimodular