`BookProof.FockNumberPreservingGap.fock_gap_of_number_preserving` {col : ℕ → (ℕ →₀ ℂ)} {mu : ℝ} (hmu : 0 ≤ mu) (hgap : IsPosCol (shiftCol col mu)) {u : FockAlg} (h0 : u 0 = 0) : mu

Initializing...

`BookProof.FockNumberPreservingGap.fock_gap_of_number_preserving` {col : ℕ → (ℕ →₀ ℂ)} {mu : ℝ} (hmu : 0 ≤ mu) (hgap : IsPosCol (shiftCol col mu)) {u : FockAlg} (h0 : u 0 = 0) : mu · Prove2Me