English
If x commutes with y, then p.smeval x and q.smeval y commute: Commute (p.smeval x) (q.smeval y).
Русский
Если x коммутирует с y, то p.smeval x и q.smeval y коммутируют: Commute (p.smeval x) (q.smeval y).
LaTeX
$$Commute x y \rightarrow Commute (p.smeval x) (q.smeval y)$$
Lean4
theorem smeval_commute (hc : Commute x y) : Commute (p.smeval x) (q.smeval y) := by
induction p using Polynomial.induction_on' with
| add r s hr hs => exact (smeval_add R r s x) ▸ Commute.add_left hr hs
| monomial n a =>
simp only [smeval_monomial]
refine Commute.smul_left ?_ a
induction n with
| zero => simp only [npow_zero, Commute.one_left]
| succ n ih =>
refine (commute_iff_eq (x ^ (n + 1)) (q.smeval y)).mpr ?_
rw [commute_iff_eq (x ^ n) (q.smeval y)] at ih
have hxq : x * q.smeval y = q.smeval y * x :=
by
refine (commute_iff_eq x (q.smeval y)).mp ?_
exact Commute.symm (smeval_commute_left R q (Commute.symm hc))
rw [pow_succ, ← mul_assoc, ← ih, mul_assoc, hxq, mul_assoc]
