`BookProof.ChapterGaugeUnconstrainedSpectrum.permOp_basisVec` [DecidableEq X] (σ : Equiv.Perm X) (y : X) : permOp σ (basisVec y) = basisVec (σ y)

Initializing...

`BookProof.ChapterGaugeUnconstrainedSpectrum.permOp_basisVec` [DecidableEq X] (σ : Equiv.Perm X) (y : X) : permOp σ (basisVec y) = basisVec (σ y) · Prove2Me