IntegerRank.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.matrix_rank_le_of_independent_imp line 14

Source documentation

Comparing all finite column families compares matrix ranks.

theorem matrix_rank_le_of_independent_imp
    {m : Type u} {n : Type v} [Fintype m] [Fintype n]
    {K : Type w} {L : Type x} [Field K] [Field L]
    (A : Matrix m n K) (B : Matrix m n L)
    (h : ∀ (r : ℕ) (f : Fin r → n), LinearIndependent K (A.col ∘ f) →
      LinearIndependent L (B.col ∘ f)) : A.rank ≤ B.rank := by
…

theorem OAI.Problem335.matrix_rank_eq_of_independent_iff line 38

Source documentation

Matrices with the same finite-column dependence relations have equal ranks.

theorem matrix_rank_eq_of_independent_iff
    {m : Type u} {n : Type v} [Fintype m] [Fintype n]
    {K : Type w} {L : Type x} [Field K] [Field L]
    (A : Matrix m n K) (B : Matrix m n L)
    (h : ∀ (r : ℕ) (f : Fin r → n), LinearIndependent K (A.col ∘ f) ↔
      LinearIndependent L (B.col ∘ f)) : A.rank = B.rank := by
…

theorem OAI.Problem335.matrix_rank_algebraMap_eq line 50

Source documentation

Extending an integral coefficient matrix to either of two faithful field extensions gives the same rank. The fields need not embed into each other.

theorem matrix_rank_algebraMap_eq
    {m : Type u} {n : Type v} [Fintype m] [Fintype n]
    {R K L : Type*} [CommRing R] [Field K] [Field L]
    [Algebra R K] [Algebra R L] [FaithfulSMul R K] [FaithfulSMul R L]
    (A : Matrix m n R) :
    (A.map (algebraMap R K)).rank = (A.map (algebraMap R L)).rank := by
…

theorem OAI.Problem335.matrix_rank_map line 63

Source documentation

A field embedding preserves the rank of a finite rectangular matrix.

theorem matrix_rank_map
    {m : Type u} {n : Type v} [Fintype m] [Fintype n]
    {F K : Type*} [Field F] [Field K] (f : F →+* K) (A : Matrix m n F) :
    (A.map f).rank = A.rank := by
…

theorem OAI.Problem335.integer_matrix_rank_eq line 71

Source documentation

Integer matrices have the same rank over any two characteristic-zero fields.

theorem integer_matrix_rank_eq
    {m : Type u} {n : Type v} [Fintype m] [Fintype n]
    (K L : Type*) [Field K] [CharZero K] [Field L] [CharZero L]
    (A : Matrix m n ℤ) :
    (A.map (Int.castRingHom K)).rank = (A.map (Int.castRingHom L)).rank := by
…

theorem OAI.Problem335.integer_matrix_rank_eq_complex line 79

Source documentation

The characteristic-zero rank-transfer step used in the lower bound.

theorem integer_matrix_rank_eq_complex
    {m : Type u} {n : Type v} [Fintype m] [Fintype n]
    (K : Type*) [Field K] [CharZero K] (A : Matrix m n ℤ) :
    (A.map (Int.castRingHom K)).rank = (A.map (Int.castRingHom ℂ)).rank := by
…