English
For all i, (x · p^n).coeff (m+n) = x.coeff m^{p^n}.
Русский
Для всех i выполняется (x · p^n).coeff (m+n) = x.coeff m^{p^n}.
LaTeX
$$$ (x \cdot p^{n}).coeff (m + n) = x.coeff m ^ {p^{n}} $$$
Lean4
theorem iterate_verschiebung_mul (x y : 𝕎 R) (i j : ℕ) :
verschiebung^[i] x * verschiebung^[j] y = verschiebung^[i + j] (frobenius^[j] x * frobenius^[i] y) :=
by
calc
_ = verschiebung^[i] (x * frobenius^[i] (verschiebung^[j] y)) := ?_
_ = verschiebung^[i] (x * verschiebung^[j] (frobenius^[i] y)) := ?_
_ = verschiebung^[i] (verschiebung^[j] (frobenius^[i] y) * x) := ?_
_ = verschiebung^[i] (verschiebung^[j] (frobenius^[i] y * frobenius^[j] x)) := ?_
_ = verschiebung^[i + j] (frobenius^[i] y * frobenius^[j] x) := ?_
_ = _ := ?_
· apply iterate_verschiebung_mul_left
· rw [verschiebung_frobenius_comm.iterate_iterate]
· rw [mul_comm]
· rw [iterate_verschiebung_mul_left]
· rw [iterate_add_apply]
· rw [mul_comm]
