R : Type u
S : Type ?u.4503
inst✝ : Semiring R
n : WithBot ℕ
f : R[X]
⊢ (∀ (i : ℕ), ↑i > n → ↑(lcoeff R i) f = 0) ↔ ∀ (m : ℕ), n < ↑m → coeff f m = 0
R : Type u
S : Type ?u.4503
inst✝ : Semiring R
n : WithBot ℕ
f : R[X]
⊢ f ∈ degreeLE R n ↔ degree f ≤ n
simp only [degreeLE, Submodule.mem_iInf, degree_le_iff_coeff_zero, LinearMap.mem_ker]
no goals
R : Type u
S : Type ?u.4503
inst✝ : Semiring R
n : WithBot ℕ
f : R[X]
⊢ (∀ (i : ℕ), ↑i > n → ↑(lcoeff R i) f = 0) ↔ ∀ (m : ℕ), n < ↑m → coeff f m = 0
rfl