`BookProof.HermiteBandHigher.Band.monoG` {T : MvPolynomial (Fin d) ℂ →ₗ[ℂ] MvPolynomial (Fin d) ℂ} {r M : ℕ} {C : ℝ} {g g' : ℕ → ℝ} (hC : 0 ≤ C) (hg : ∀ n, g n ≤ g' n)...

Initializing...

`BookProof.HermiteBandHigher.Band.monoG` {T : MvPolynomial (Fin d) ℂ →ₗ[ℂ] MvPolynomial (Fin d) ℂ} {r M : ℕ} {C : ℝ} {g g' : ℕ → ℝ} (hC : 0 ≤ C) (hg : ∀ n, g n ≤ g' n)... · Prove2Me