constantCoeff_wittStructureInt_zero

English

For Φ ∈ MvPolynomial idx ℤ, the constant coefficient of WittStructureInt p Φ 0 equals the constant coefficient of Φ.

Русский

Для Φ ∈ MvPolynomial idx ℤ константный коэффициент WittStructureInt p Φ 0 равен константному коэффициенту Φ.

LaTeX

$$$\\operatorname{constantCoeff}(\\mathrm{wittStructureInt}\\, p \\, Φ \\, 0) = \\operatorname{constantCoeff} Φ$$$

Lean4

@[simp]
theorem constantCoeff_wittStructureInt_zero (Φ : MvPolynomial idx ℤ) :
    constantCoeff (wittStructureInt p Φ 0) = constantCoeff Φ :=
  by
  have inj : Function.Injective (Int.castRingHom ℚ) := by intro m n; exact Int.cast_inj.mp
  apply inj
  rw [← constantCoeff_map, map_wittStructureInt, constantCoeff_wittStructureRat_zero, constantCoeff_map]

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