Documentation

Mathlib.LinearAlgebra.Matrix.Integer

Lemmas on integer matrices #

Here we collect some results about matrices over ℚ and ℤ.

Main definitions and results #

TODO #

Consider generalizing these constructions to matrices over localizations of rings (or semirings).

Casts #

These results are useful shortcuts because the canonical casting maps out of ℕ, ℤ, and ℚ to suitable types are bare functions, not ring homs, so we cannot apply Matrix.map_mul directly to them.

source
theorem Matrix.map_mul_natCast {n : Type u_2} [Fintype n] {α : Type u_3} [NonAssocSemiring α] (A B : Matrix n n ℕ) :
(A * B).map Nat.cast = A.map Nat.cast * B.map Nat.cast
source
theorem Matrix.map_mul_intCast {n : Type u_2} [Fintype n] {α : Type u_3} [NonAssocRing α] (A B : Matrix n n ℤ) :
(A * B).map Int.cast = A.map Int.cast * B.map Int.cast
source
theorem Matrix.map_mul_ratCast {n : Type u_2} [Fintype n] {α : Type u_3} [DivisionRing α] [CharZero α] (A B : Matrix n n ℚ) :
(A * B).map Rat.cast = A.map Rat.cast * B.map Rat.cast

Denominator of a rational matrix #

source
def Matrix.den {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m n ℚ) :
ℕ

The denominator of a matrix of rationals (as a Nat, defined as the LCM of the denominators of the entries).

Equations
Instances For
    source
    def Matrix.num {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m n ℚ) :
    Matrix m n ℤ

    The numerator of a matrix of rationals (a matrix of integers, defined so that A.num / A.den = A).

    Equations
    Instances For
      source
      theorem Matrix.den_ne_zero {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m n ℚ) :
      A.den ≠ 0
      source
      theorem Matrix.num_eq_zero_iff {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m n ℚ) :
      A.num = 0 ↔ A = 0
      source
      theorem Matrix.den_dvd_iff {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] {A : Matrix m n ℚ} {r : ℕ} :
      A.den ∣ r ↔ ∀ (i : m) (j : n), (A i j).den ∣ r
      source
      theorem Matrix.num_div_den {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m n ℚ) (i : m) (j : n) :
      ↑(A.num i j) / ↑A.den = A i j
      source
      theorem Matrix.inv_denom_smul_num {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m n ℚ) :
      (↑A.den)⁻¹ • A.num.map Int.cast = A
      source
      @[simp]
      theorem Matrix.den_neg {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m n ℚ) :
      (-A).den = A.den
      source
      @[simp]
      theorem Matrix.num_neg {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m n ℚ) :
      (-A).num = -A.num
      source
      @[simp]
      theorem Matrix.den_transpose {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m n ℚ) :
      A.transpose.den = A.den
      source
      @[simp]
      theorem Matrix.num_transpose {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m n ℚ) :
      A.transpose.num = A.num.transpose

      Compatibility with map #

      source
      @[simp]
      theorem Matrix.den_map_intCast {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m n ℤ) :
      (A.map Int.cast).den = 1
      source
      @[simp]
      theorem Matrix.num_map_intCast {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m n ℤ) :
      (A.map Int.cast).num = A
      source
      @[simp]
      theorem Matrix.den_map_natCast {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m n ℕ) :
      (A.map Nat.cast).den = 1
      source
      @[simp]
      theorem Matrix.num_map_natCast {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m n ℕ) :
      (A.map Nat.cast).num = A.map Nat.cast

      Casts from scalar types #

      source
      @[simp]
      theorem Matrix.den_natCast {m : Type u_1} [Fintype m] [DecidableEq m] (a : ℕ) :
      (↑a).den = 1
      source
      @[simp]
      theorem Matrix.num_natCast {m : Type u_1} [Fintype m] [DecidableEq m] (a : ℕ) :
      (↑a).num = ↑a
      source
      @[simp]
      theorem Matrix.den_ofNat {m : Type u_1} [Fintype m] [DecidableEq m] (a : ℕ) [a.AtLeastTwo] :
      (OfNat.ofNat a).den = 1
      source
      @[simp]
      theorem Matrix.num_ofNat {m : Type u_1} [Fintype m] [DecidableEq m] (a : ℕ) [a.AtLeastTwo] :
      (OfNat.ofNat a).num = ↑a
      source
      @[simp]
      theorem Matrix.den_intCast {m : Type u_1} [Fintype m] [DecidableEq m] (a : ℤ) :
      (↑a).den = 1
      source
      @[simp]
      theorem Matrix.num_intCast {m : Type u_1} [Fintype m] [DecidableEq m] (a : ℤ) :
      (↑a).num = ↑a
      source
      @[simp]
      theorem Matrix.den_zero {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] :
      Matrix.den 0 = 1
      source
      @[simp]
      theorem Matrix.num_zero {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] :
      Matrix.num 0 = 0
      source
      @[simp]
      theorem Matrix.den_one {m : Type u_1} [Fintype m] [DecidableEq m] :
      Matrix.den 1 = 1
      source
      @[simp]
      theorem Matrix.num_one {m : Type u_1} [Fintype m] [DecidableEq m] :
      Matrix.num 1 = 1