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

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

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
a b c : Polynomial n ord
⊢ (a + b) * c = a * c + b * c
Tactic:
have rl_mul := t_mul_comm (a + b) c
State after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
a b c : Polynomial n ord
rl_mul : (a + b) * c = c * (a + b)
⊢ (a + b) * c = a * c + b * c

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
a b c : Polynomial n ord
rl_mul : (a + b) * c = c * (a + b)
⊢ (a + b) * c = a * c + b * c
Tactic:
simp [rl_mul, t_left_distrib, t_mul_comm]
State after:
no goals