Documentation

Mathlib.LinearAlgebra.Matrix.Swap

Swap matrices #

A swap matrix indexed by i and j is the matrix that, when multiplying another matrix on the left (resp. on the right), swaps the i-th row with the j-th row (resp. the i-th column with the j-th column).

Swap matrices are a special case of elementary matrices. For transvections see Mathlib/LinearAlgebra/Matrix/Transvection.lean.

Implementation detail #

This is a thin wrapper around (Equiv.swap i j).permMatrix.

source
🔸 coverage
def Matrix.swap (R : Type u_1) {n : Type u_2} [Zero R] [One R] [DecidableEq n] (i j : n) :
Matrix n n R

The swap matrix swap R i j is the identity matrix with the i-th and j-th rows modified such that multiplying by it on the left (resp. right) corresponds to swapping the i-th and j-th row (resp. column).

Equations
    Instances For
      source
      📐 coverage
      theorem Matrix.swap_comm {R : Type u_1} {n : Type u_2} [Zero R] [One R] [DecidableEq n] (i j : n) :
      swap R i j = swap R j i
      source
      📐 coverage
      @[simp]
      theorem Matrix.transpose_swap {R : Type u_1} {n : Type u_2} [Zero R] [One R] [DecidableEq n] (i j : n) :
      (swap R i j).transpose = swap R i j
      source
      📐 coverage
      @[simp]
      theorem Matrix.conjTranspose_swap {n : Type u_2} [DecidableEq n] {R : Type u_3} [NonAssocSemiring R] [StarRing R] (i j : n) :
      (swap R i j).conjTranspose = swap R i j
      source
      📐 coverage
      @[simp]
      theorem Matrix.map_swap {R : Type u_1} {n : Type u_2} [Semiring R] [DecidableEq n] {S : Type u_4} [NonAssocSemiring S] (f : R →+* S) (i j : n) :
      (swap R i j).map ⇑f = swap S i j
      source
      📐 coverage
      theorem Matrix.swap_mulVec {R : Type u_1} {n : Type u_2} [Semiring R] [DecidableEq n] [Fintype n] (i j : n) (a : n → R) :
      (swap R i j).mulVec a = a ∘ ⇑(Equiv.swap i j)
      source
      📐 coverage
      theorem Matrix.vecMul_swap {R : Type u_1} {n : Type u_2} [Semiring R] [DecidableEq n] [Fintype n] (i j : n) (a : n → R) :
      vecMul a (swap R i j) = a ∘ ⇑(Equiv.swap i j)
      source
      📐 coverage
      @[simp]
      theorem Matrix.swap_mulVec_apply {R : Type u_1} {n : Type u_2} [Semiring R] [DecidableEq n] [Fintype n] (i j : n) (a : n → R) :
      (swap R i j).mulVec a i = a j
      source
      📐 coverage
      @[simp]
      theorem Matrix.vecMul_swap_apply {R : Type u_1} {n : Type u_2} [Semiring R] [DecidableEq n] [Fintype n] (i j : n) (a : n → R) :
      vecMul a (swap R i j) i = a j
      source
      📐 coverage
      @[simp]
      theorem Matrix.swap_mul_apply_left {R : Type u_1} {n : Type u_2} {m : Type u_3} [Semiring R] [DecidableEq n] [Fintype n] (i j : n) (a : m) (g : Matrix n m R) :
      (swap R i j * g) i a = g j a

      Multiplying with swap R i j on the left swaps the i-th row with the j-th row.

      source
      📐 coverage
      @[simp]
      theorem Matrix.swap_mul_apply_right {R : Type u_1} {n : Type u_2} {m : Type u_3} [Semiring R] [DecidableEq n] [Fintype n] (i j : n) (a : m) (g : Matrix n m R) :
      (swap R i j * g) j a = g i a

      Multiplying with swap R i j on the left swaps the j-th row with the i-th row.

      source
      📐 coverage
      theorem Matrix.swap_mul_of_ne {R : Type u_1} {n : Type u_2} {m : Type u_3} [Semiring R] [DecidableEq n] [Fintype n] {i j a : n} {b : m} (hai : a ≠ i) (haj : a ≠ j) (g : Matrix n m R) :
      (swap R i j * g) a b = g a b
      source
      📐 coverage
      @[simp]
      theorem Matrix.mul_swap_apply_left {R : Type u_1} {n : Type u_2} {m : Type u_3} [Semiring R] [DecidableEq n] [Fintype n] (i j : n) (a : m) (g : Matrix m n R) :
      (g * swap R i j) a i = g a j

      Multiplying with swap R i j on the right swaps the i-th column with the j-th column.

      source
      📐 coverage
      @[simp]
      theorem Matrix.mul_swap_apply_right {R : Type u_1} {n : Type u_2} {m : Type u_3} [Semiring R] [DecidableEq n] [Fintype n] (i j : n) (a : m) (g : Matrix m n R) :
      (g * swap R i j) a j = g a i

      Multiplying with swap R i j on the right swaps the j-th column with the i-th column.

      source
      📐 coverage
      theorem Matrix.mul_swap_of_ne {R : Type u_1} {n : Type u_2} {m : Type u_3} [Semiring R] [DecidableEq n] [Fintype n] {i j b : n} {a : m} (hbi : b ≠ i) (hbj : b ≠ j) (g : Matrix m n R) :
      (g * swap R i j) a b = g a b
      source
      📐 coverage
      theorem Matrix.swap_mul_self {R : Type u_1} {n : Type u_2} [Semiring R] [DecidableEq n] [Fintype n] (i j : n) :
      swap R i j * swap R i j = 1

      Swap matrices are self inverse.

      source
      🔸 coverage
      def Matrix.GeneralLinearGroup.swap (R : Type u_1) {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] (i j : n) :
      GL n R

      Matrix.swap as an element of GL n R.

      Equations
        Instances For
          source
          📐 coverage
          @[simp]
          theorem Matrix.GeneralLinearGroup.val_swap (R : Type u_1) {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] (i j : n) :
          ↑(swap R i j) = Matrix.swap R i j
          source
          📐 coverage
          @[simp]
          theorem Matrix.GeneralLinearGroup.val_inv_swap (R : Type u_1) {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] (i j : n) :
          ↑(swap R i j)⁻¹ = Matrix.swap R i j
          source
          📐 coverage
          @[simp]
          theorem Matrix.GeneralLinearGroup.map_swap {R : Type u_1} {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] {S : Type u_3} [CommRing S] (f : R →+* S) (i j : n) :
          (map f) (swap R i j) = swap S i j