`BookProof.HermiteBandHigher.isBandR_zero_op` (r m : ℕ) : IsBandR r m (0 : MvPolynomial (Fin d) ℂ →ₗ[ℂ] MvPolynomial (Fin d) ℂ)

Initializing...

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