Theorems · Theorem · commutative algebra

MvPowerSeries.coeff_truncFinset_mul_truncFinset_eq_coeff_mul

∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {s : Finset (σ →₀ ℕ)},
  IsLowerSet ↑s →
    ∀ {x : σ →₀ ℕ} (f g : MvPowerSeries σ R),
      x ∈ s →
        MvPolynomial.coeff x ((MvPowerSeries.truncFinset R s) f * (MvPowerSeries.truncFinset R s) g) =
          (MvPowerSeries.coeff x) (f * g)

Defined in

Mathlib.RingTheory.MvPowerSeries.Trunc

Cited by

2 results in Mathlib

Foundations

Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiring