`BookProof.ChapterGaugeUnconstrainedSpectrum.permOp_isFunctionOfSpectrum_iff` (σ : Equiv.Perm X) : IsFunctionOfSpectrum (permOp σ) ↔ σ = 1

Initializing...

`BookProof.ChapterGaugeUnconstrainedSpectrum.permOp_isFunctionOfSpectrum_iff` (σ : Equiv.Perm X) : IsFunctionOfSpectrum (permOp σ) ↔ σ = 1 · Prove2Me