iterate_verschiebung_mul_left — Mathlib

English

In CharP context, (x · p^n).coeff m = 0 whenever m < n.

Русский

В контексте CharP, коэффициент (м) у (x · p^n) равен 0 при m < n.

LaTeX

$$$ (x \cdot p^{n}).coeff m = 0 \quad \text{if } m < n $$$

Lean4

theorem iterate_verschiebung_mul_left (x y : 𝕎 R) (i : ℕ) :
    verschiebung^[i] x * y = verschiebung^[i] (x * frobenius^[i] y) := by
  induction i generalizing y with
  | zero => simp
  | succ i ih => rw [iterate_succ_apply', ← verschiebung_mul_frobenius, ih, iterate_succ_apply', iterate_succ_apply]

Похожие утверждения