no goals
R : Type u
S : Type ?u.28643
inst✝ : Semiring R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
⊢ ↑(degreeLTEquiv R n) { val := p, property := hp } = 0 ↔ p = 0
rw [LinearEquiv.map_eq_zero_iff, Submodule.mk_eq_zero]