ghostComponent_verschiebungFun — Mathlib

English

For all n, ghostComponent(n+1)(verschiebungFun x) equals p times ghostComponent(n)(x).

Русский

Для всех n ghostComponent(n+1)(verschiebungFun x) равно p умножить на ghostComponent(n)(x).

LaTeX

$$$$ ghostComponent_{n+1}(\\\\text{verschiebungFun}(x)) = p \\cdot ghostComponent_{n}(x). $$$$

Lean4

@[ghost_simps]
theorem ghostComponent_verschiebungFun [hp : Fact p.Prime] (x : 𝕎 R) (n : ℕ) :
    ghostComponent (n + 1) (verschiebungFun x) = p * ghostComponent n x :=
  by
  simp only [ghostComponent_apply, aeval_wittPolynomial]
  rw [Finset.sum_range_succ', verschiebungFun_coeff, if_pos rfl, zero_pow (pow_ne_zero _ hp.1.ne_zero), mul_zero,
    add_zero, Finset.mul_sum, Finset.sum_congr rfl]
  rintro i -
  simp only [pow_succ', verschiebungFun_coeff_succ, Nat.succ_sub_succ_eq_sub, mul_assoc]

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