Documentation

TauCeti.LinearAlgebra.Matrix.Antitranspose

The antitranspose of a square matrix #

The antitranspose of a square matrix A indexed by Fin m is its reflection in the antidiagonal, Aᴬ i j = A (rev j) (rev i); for 2 × 2 matrices it sends (a b; c d) to (d b; c a). Over a commutative ring it reverses products and preserves determinants, so it is an anti-involution of the matrix ring and of the special linear group.

Main declarations #

source
def Matrix.antitranspose {α : Type u_1} {m : ℕ} (A : Matrix (Fin m) (Fin m) α) :
Matrix (Fin m) (Fin m) α

The antitranspose of a square matrix: its reflection in the antidiagonal, A.antitranspose i j = A (rev j) (rev i).

Instances For
    source
    @[simp]
    theorem Matrix.antitranspose_apply {α : Type u_1} {m : ℕ} (A : Matrix (Fin m) (Fin m) α) (i j : Fin m) :
    A.antitranspose i j = A j.rev i.rev
    source
    @[simp]
    theorem Matrix.antitranspose_antitranspose {α : Type u_1} {m : ℕ} (A : Matrix (Fin m) (Fin m) α) :
    A.antitranspose.antitranspose = A
    source
    @[simp]
    theorem Matrix.antitranspose_zero {α : Type u_1} {m : ℕ} [Zero α] :
    antitranspose 0 = 0
    source
    @[simp]
    theorem Matrix.antitranspose_one {α : Type u_1} {m : ℕ} [Zero α] [One α] :
    antitranspose 1 = 1
    source
    @[simp]
    theorem Matrix.antitranspose_add {α : Type u_1} {m : ℕ} [Add α] (A B : Matrix (Fin m) (Fin m) α) :
    (A + B).antitranspose = A.antitranspose + B.antitranspose
    source
    @[simp]
    theorem Matrix.antitranspose_neg {α : Type u_1} {m : ℕ} [Neg α] (A : Matrix (Fin m) (Fin m) α) :
    (-A).antitranspose = -A.antitranspose
    source
    @[simp]
    theorem Matrix.antitranspose_sub {α : Type u_1} {m : ℕ} [Sub α] (A B : Matrix (Fin m) (Fin m) α) :
    (A - B).antitranspose = A.antitranspose - B.antitranspose
    source
    @[simp]
    theorem Matrix.antitranspose_smul {α : Type u_1} {m : ℕ} {β : Type u_2} [SMul β α] (c : β) (A : Matrix (Fin m) (Fin m) α) :
    (c • A).antitranspose = c • A.antitranspose
    source
    theorem Matrix.antitranspose_mul {α : Type u_1} {m : ℕ} [AddCommMonoid α] [CommMagma α] (A B : Matrix (Fin m) (Fin m) α) :
    (A * B).antitranspose = B.antitranspose * A.antitranspose

    The antitranspose reverses products.

    source
    @[simp]
    theorem Matrix.det_antitranspose {m : ℕ} {R : Type u_2} [CommRing R] (A : Matrix (Fin m) (Fin m) R) :
    A.antitranspose.det = A.det

    The antitranspose preserves determinants.

    source
    theorem Matrix.antitranspose_fin_two {α : Type u_1} (A : Matrix (Fin 2) (Fin 2) α) :
    A.antitranspose = !![A 1 1, A 0 1; A 1 0, A 0 0]

    The antitranspose of (a b; c d) is (d b; c a).