`BookProof.HermiteBandHigher.isBandDeg_zero_op` (m : ℕ) : IsBandDeg m (0 : MvPolynomial (Fin d) ℂ →ₗ[ℂ] MvPolynomial (Fin d) ℂ)

Initializing...

`BookProof.HermiteBandHigher.isBandDeg_zero_op` (m : ℕ) : IsBandDeg m (0 : MvPolynomial (Fin d) ℂ →ₗ[ℂ] MvPolynomial (Fin d) ℂ) · Prove2Me