Permutation matrices

This file defines the matrix associated with a permutation

Main definitions

• Equiv.Perm.permMatrix: the permutation matrix associated with an Equiv.Perm

Main results

• Matrix.det_permutation: the determinant is the sign of the permutation
• Matrix.trace_permutation: the trace is the number of fixed points of the permutation

@[reducible, inline]

abbrev Equiv.Perm.permMatrix {n : Type u_1} (R : Type u_2) [DecidableEq n] (σ : Equiv.Perm n) [Zero R] [One R] : Matrix n n R

the permutation matrix associated with an Equiv.Perm

Equations

• Equiv.Perm.permMatrix R σ = (Equiv.toPEquiv σ).toMatrix

@[simp]

theorem Matrix.det_permutation {n : Type u_1} {R : Type u_2} [DecidableEq n] [Fintype n] (σ : Equiv.Perm n) [CommRing R] : (Equiv.Perm.permMatrix R σ).det = ↑↑(Equiv.Perm.sign σ)

The determinant of a permutation matrix equals its sign.

theorem Matrix.trace_permutation {n : Type u_1} {R : Type u_2} [DecidableEq n] [Fintype n] (σ : Equiv.Perm n) [AddCommMonoidWithOne R] : (Equiv.Perm.permMatrix R σ).trace = ↑(Function.fixedPoints ⇑σ).ncard

The trace of a permutation matrix equals the number of fixed points.