constantCoeff_wittStructureInt — Mathlib

English

Let Φ ∈ MvPolynomial idx ℤ with constantCoeff Φ = 0. Then for every n, constantCoeff (wittStructureInt p Φ n) = 0.

Русский

Пусть Φ ∈ MvPolynomial idx ℤ с constantCoeff Φ = 0. Тогда для каждого n верно constantCoeff (wittStructureInt p Φ n) = 0.

LaTeX

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

Lean4

theorem constantCoeff_wittStructureInt (Φ : MvPolynomial idx ℤ) (h : constantCoeff Φ = 0) (n : ℕ) :
    constantCoeff (wittStructureInt p Φ n) = 0 :=
  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, RingHom.map_zero]
  rw [constantCoeff_map, h, RingHom.map_zero]

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