ghostComponent_zero_verschiebungFun

English

The ghost component at index 0 of verschiebungFun x is zero.

Русский

Г ghosts-компонента на позиции 0 для verschiebungFun x равна нулю.

LaTeX

$$$$ ghostComponent_0(\\\\text{verschiebungFun}(x)) = 0. $$$$

Lean4

@[ghost_simps]
theorem ghostComponent_zero_verschiebungFun [hp : Fact p.Prime] (x : 𝕎 R) : ghostComponent 0 (verschiebungFun x) = 0 :=
  by
  rw [ghostComponent_apply, aeval_wittPolynomial, Finset.range_one, Finset.sum_singleton, verschiebungFun_coeff_zero,
    pow_zero, pow_zero, pow_one, one_mul]

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