Theorems · Theorem · commutative algebra

MvPowerSeries.support_expand

∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : MvPowerSeries σ R),
  Function.support ((MvPowerSeries.expand p hp) φ) = (fun x => p • x) '' Function.support φ

Defined in

Mathlib.RingTheory.MvPowerSeries.Expand

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRing