R : Type u_1
inst✝ : CommSemiring R
n m : ℕ
⊢ (if m < n then 0 else 0) = 0
R : Type u_1
inst✝ : CommSemiring R
n m : ℕ
⊢ Polynomial.coeff (trunc n 0) m = Polynomial.coeff 0 m
rw [coeff_trunc, LinearMap.map_zero, Polynomial.coeff_zero]
no goals
R : Type u_1
inst✝ : CommSemiring R
n m : ℕ
⊢ (if m < n then 0 else 0) = 0
split_ifs <;> rfl