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

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

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