intros
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible : Polynomial n ord
dividers : List (Polynomial n ord)
⊢ divisible ∈ asIdeal dividers → 0 ∈ asIdeal dividers
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible : Polynomial n ord
dividers : List (Polynomial n ord)
a✝ : divisible ∈ asIdeal dividers
⊢ 0 ∈ asIdeal dividers