wittStructureInt_vars — Mathlib

English

If idx is finite, Φ ∈ MvPolynomial idx ℤ, then (wittStructureInt p Φ n).vars ⊆ univ ×ˢ range(n+1).

Русский

Если idx конечен, то (wittStructureInt p Φ n).vars ⊆ univ ×ˢ range(n+1).

LaTeX

$$$(\\mathrm{wittStructureInt}\\ p \\ Φ \\ n).\\mathrm{vars} \\subseteq \\mathrm{Finset.univ} \\timesˢ \\mathrm{Finset.range}(n+1)$$$

Lean4

theorem wittStructureInt_vars [Fintype idx] (Φ : MvPolynomial idx ℤ) (n : ℕ) :
    (wittStructureInt p Φ n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1) :=
  by
  have : Function.Injective (Int.castRingHom ℚ) := Int.cast_injective
  rw [← vars_map_of_injective _ this, map_wittStructureInt]
  apply wittStructureRat_vars

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