`BookProof.FockNumberPreservingGap.isPosCol_shiftCol_diagCol` {e : ℕ → ℝ} {mu : ℝ} (he : ∀ k, mu ≤ e k) : IsPosCol (shiftCol (diagCol e) mu)

Initializing...

`BookProof.FockNumberPreservingGap.isPosCol_shiftCol_diagCol` {e : ℕ → ℝ} {mu : ℝ} (he : ∀ k, mu ≤ e k) : IsPosCol (shiftCol (diagCol e) mu) · Prove2Me