Elementary row operations

This file defines row-scaling matrices and row-equivalence.

Main definitions

• Matrix.rowScale i c: the elementary matrix which scales row i by c
• Matrix.RowEquivalent A B: row-equivalence by left multiplication by an element of GL

def Matrix.rowScale {R : Type u_1} {m : Type u_2} [DecidableEq m] [Zero R] [One R] (i : m) (c : R) : Matrix m m R

The elementary matrix scaling row i by c.

Equations

• Matrix.rowScale i c = Matrix.diagonal (Pi.mulSingle i c)

@[simp]

theorem Matrix.rowScale_one {R : Type u_1} {m : Type u_2} [DecidableEq m] [Zero R] [One R] (i : m) : rowScale i 1 = 1

@[simp]

theorem Matrix.rowScale_apply_same {R : Type u_1} {m : Type u_2} [DecidableEq m] [Zero R] [One R] (i : m) (c : R) : rowScale i c i i = c

@[simp]

theorem Matrix.rowScale_apply_diag_of_ne {R : Type u_1} {m : Type u_2} [DecidableEq m] [Zero R] [One R] {i a : m} (h : a ≠ i) (c : R) : rowScale i c a a = 1

@[simp]

theorem Matrix.rowScale_apply_ne {R : Type u_1} {m : Type u_2} [DecidableEq m] [Zero R] [One R] {i a b : m} (hab : a ≠ b) (c : R) : rowScale i c a b = 0

theorem Matrix.rowScale_mul {R : Type u_1} {m : Type u_2} {n : Type u_3} [DecidableEq m] [CommRing R] [Fintype m] (i : m) (c : R) (M : Matrix m n R) : rowScale i c * M = M.updateRow i (c • M.row i)

theorem Matrix.mul_rowScale {R : Type u_1} {m : Type u_2} {n : Type u_3} [DecidableEq m] [CommRing R] [Fintype m] (i : m) (c : R) (M : Matrix n m R) : M * rowScale i c = M.updateCol i (c • M.col i)

@[simp]

theorem Matrix.rowScale_mul_rowScale {R : Type u_1} {m : Type u_2} [DecidableEq m] [CommRing R] [Fintype m] (i : m) (c d : R) : rowScale i c * rowScale i d = rowScale i (c * d)

def Matrix.GeneralLinearGroup.rowScale {R : Type u_1} {m : Type u_2} [DecidableEq m] [CommRing R] [Fintype m] (i : m) (c : Rˣ) : GL m R

Matrix.rowScale as an element of GL m R.

Equations

• Matrix.GeneralLinearGroup.rowScale i c = { val := Matrix.rowScale i ↑c, inv := Matrix.rowScale i ↑c⁻¹, val_inv := ⋯, inv_val := ⋯ }

@[simp]

theorem Matrix.GeneralLinearGroup.val_rowScale {R : Type u_1} {m : Type u_2} [DecidableEq m] [CommRing R] [Fintype m] (i : m) (c : Rˣ) : ↑(rowScale i c) = Matrix.rowScale i ↑c

@[simp]

theorem Matrix.GeneralLinearGroup.map_rowScale {R : Type u_1} {m : Type u_2} [DecidableEq m] [CommRing R] [Fintype m] {S : Type u_4} [CommRing S] (f : R →+* S) (i : m) (c : Rˣ) : (map f) (rowScale i c) = rowScale i ((Units.map ↑f) c)

def Matrix.GeneralLinearGroup.transvection {R : Type u_1} {m : Type u_2} [DecidableEq m] [CommRing R] [Fintype m] (i j : m) (h : i ≠ j) (c : R) : GL m R

Matrix.transvection as an element of GL.

Equations

• Matrix.GeneralLinearGroup.transvection i j h c = { val := Matrix.transvection i j c, inv := Matrix.transvection i j (-c), val_inv := ⋯, inv_val := ⋯ }

@[simp]

theorem Matrix.GeneralLinearGroup.val_transvection {R : Type u_1} {m : Type u_2} [DecidableEq m] [CommRing R] [Fintype m] (i j : m) (h : i ≠ j) (c : R) : ↑(transvection i j h c) = Matrix.transvection i j c

@[reducible, inline]

abbrev Matrix.RowEquivalent {R : Type u_1} {m : Type u_2} {n : Type u_3} [DecidableEq m] [CommRing R] [Fintype m] (A B : Matrix m n R) : Prop

Row-equivalence via the left action of GL m R on Matrix m n R.

Equations

• A.RowEquivalent B = (B ∈ MulAction.orbit (GL m R) A)

theorem Matrix.rowEquivalent_iff_associated_op_op {R : Type u_1} {m : Type u_2} [DecidableEq m] [CommRing R] [Fintype m] {A B : Matrix m m R} : A.RowEquivalent B ↔ Associated (MulOpposite.op A) (MulOpposite.op B)

theorem Matrix.RowEquivalent.refl {R : Type u_1} {m : Type u_2} {n : Type u_3} [DecidableEq m] [CommRing R] [Fintype m] (A : Matrix m n R) : A.RowEquivalent A

theorem Matrix.RowEquivalent.symm {R : Type u_1} {m : Type u_2} {n : Type u_3} [DecidableEq m] [CommRing R] [Fintype m] {A B : Matrix m n R} (h : A.RowEquivalent B) : B.RowEquivalent A

theorem Matrix.RowEquivalent.trans {R : Type u_1} {m : Type u_2} {n : Type u_3} [DecidableEq m] [CommRing R] [Fintype m] {A B C : Matrix m n R} (hAB : A.RowEquivalent B) (hBC : B.RowEquivalent C) : A.RowEquivalent C

@[instance_reducible]

def Matrix.RowEquivalent.setoid {R : Type u_1} {m : Type u_2} {n : Type u_3} [DecidableEq m] [CommRing R] [Fintype m] : Setoid (Matrix m n R)

The row-equivalence relation as a scoped setoid instance.

Equations

• Matrix.RowEquivalent.setoid = { r := Matrix.RowEquivalent, iseqv := ⋯ }

theorem Matrix.rowEquivalent_swap {R : Type u_1} {m : Type u_2} {n : Type u_3} [DecidableEq m] [CommRing R] [Fintype m] (A : Matrix m n R) (i j : m) : A.RowEquivalent (swap R i j * A)

theorem Matrix.rowEquivalent_rowScale {R : Type u_1} {m : Type u_2} {n : Type u_3} [DecidableEq m] [CommRing R] [Fintype m] (A : Matrix m n R) (i : m) (c : Rˣ) : A.RowEquivalent (rowScale i ↑c * A)

theorem Matrix.rowEquivalent_transvection {R : Type u_1} {m : Type u_2} {n : Type u_3} [DecidableEq m] [CommRing R] [Fintype m] (A : Matrix m n R) (i j : m) (h : i ≠ j) (c : R) : A.RowEquivalent (transvection i j c * A)