`BookProof.ChapterA3n.permMat_mul` {N : ℕ} (σ τ : Equiv.Perm (Fin N)) : permMat σ * permMat τ = permMat (σ * τ)

Initializing...

`BookProof.ChapterA3n.permMat_mul` {N : ℕ} (σ τ : Equiv.Perm (Fin N)) : permMat σ * permMat τ = permMat (σ * τ) · Prove2Me