Theorem: t_mul_zero (Diploma/Algebra/PolynomialRing.lean)

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
⊢ ∀ (a : Polynomial n ord), a * 0 = 0
Tactic:
intros p
State after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
⊢ p * 0 = 0

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
⊢ p * 0 = 0
Tactic:
simp [t_mul_comm p, t_zero_mul]
State after:
no goals