Theorem: polynomial.zero_r_in_ideal (Diploma/Polynomials/Division.lean)

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

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible : Polynomial n ord
dividers : List (Polynomial n ord)
a✝ : divisible ∈ asIdeal dividers
⊢ 0 ∈ asIdeal dividers
Tactic:
simp
State after:
no goals