constantCoeff_wittStructureRat_zero

English

If Φ is a polynomial over ℚ, then the constant term of WittStructureRat p Φ 0 equals the constant term of Φ.

Русский

Если Φ — полином над полем рациональных чисел, то постоянный коэффициент WittStructureRat p Φ 0 равен постоянному коэффициенту Φ.

LaTeX

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

Lean4

@[simp]
theorem constantCoeff_wittStructureRat_zero (Φ : MvPolynomial idx ℚ) :
    constantCoeff (wittStructureRat p Φ 0) = constantCoeff Φ := by
  simp only [wittStructureRat, bind₁, map_aeval, xInTermsOfW_zero, constantCoeff_rename, constantCoeff_wittPolynomial,
    aeval_X, constantCoeff_comp_algebraMap, eval₂Hom_zero'_apply, RingHom.id_apply]

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