`BookProof.HermiteBandHigher.IsBandDeg.smul` {m : ℕ} {T : MvPolynomial (Fin d) ℂ →ₗ[ℂ] MvPolynomial (Fin d) ℂ} (c : ℂ) (hT : IsBandDeg m T) : IsBandDeg m (c • T)

Initializing...

`BookProof.HermiteBandHigher.IsBandDeg.smul` {m : ℕ} {T : MvPolynomial (Fin d) ℂ →ₗ[ℂ] MvPolynomial (Fin d) ℂ} (c : ℂ) (hT : IsBandDeg m T) : IsBandDeg m (c • T) · Prove2Me