`BookProof.ChapterGaugeUnconstrainedSpectrum.diagOp_injective` : Function.Injective (diagOp (X := X))

Initializing...

`BookProof.ChapterGaugeUnconstrainedSpectrum.diagOp_injective` : Function.Injective (diagOp (X := X)) · Prove2Me