constantCoeff_wittStructureRat — Mathlib

English

If constantCoeff Φ = 0 for a polynomial Φ over ℚ, then for every n, constantCoeff (wittStructureRat p Φ n) = 0.

Русский

Если постоянный коэффициент Φ равен нулю, то для каждого n верно constantCoeff (wittStructureRat p Φ n) = 0.

LaTeX

$$$\\text{constantCoeff} \\ Φ = 0 \\; \\Rightarrow \\; \\forall n, \\; \\text{constantCoeff}(\\mathrm{wittStructureRat}\, p \\, Φ \\, n) = 0$$$

Lean4

theorem constantCoeff_wittStructureRat (Φ : MvPolynomial idx ℚ) (h : constantCoeff Φ = 0) (n : ℕ) :
    constantCoeff (wittStructureRat p Φ n) = 0 := by
  simp only [wittStructureRat, eval₂Hom_zero'_apply, h, bind₁, map_aeval, constantCoeff_rename,
    constantCoeff_wittPolynomial, constantCoeff_comp_algebraMap, RingHom.id_apply, constantCoeff_xInTermsOfW]

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