`BookProof.FockCubicUnbounded.trial_at_other` {k n : ℕ} {c : ℝ} {m : ℕ} (h1 : m ≠ n) (h2 : m ≠ n + 3) : trial k n c (confAt k m) = 0

Initializing...

`BookProof.FockCubicUnbounded.trial_at_other` {k n : ℕ} {c : ℝ} {m : ℕ} (h1 : m ≠ n) (h2 : m ≠ n + 3) : trial k n c (confAt k m) = 0 · Prove2Me