Ideals of multivariate power series rings

TheoremMembership in the span of a constant and initial variables#✓fully proved

A power series lies in the span of C ϖ and the first k variables exactly when every coefficient of a monomial supported on the last n - k variables is divisible by ϖ.

theorem MvPowerSeries.mem_span_C_sup_ofList_take_iff {R : Type*} [CommRing R]
    (ϖ : R) (n k : ℕ) (F : MvPowerSeries (Fin n) R) :
    F ∈ Ideal.span {(C ϖ : MvPowerSeries (Fin n) R)} ⊔
        Ideal.ofList ((List.ofFn fun j : Fin n => (X j : MvPowerSeries (Fin n) R)).take k) ↔
      ∀ m : Fin n →₀ ℕ, (∀ j : Fin n, (j : ℕ) < k → m j = 0) → ϖ ∣ coeff m F

Used by 1

Used byThe variables span the kernel of the constant coefficient map

TheoremThe variables span the kernel of the constant coefficient map#✓fully proved

The kernel of the constant coefficient map on multivariate power series is the span of the variables.

theorem MvPowerSeries.span_range_X_eq_ker_constantCoeff {R : Type*} [CommRing R] (n : ℕ) :
    Ideal.span (Set.range (X : Fin n → MvPowerSeries (Fin n) R)) =
      RingHom.ker (constantCoeff : MvPowerSeries (Fin n) R →+* R)

Uses 1

Proof usesMembership in the span of a constant and initial variables

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.