Theorems · Theorem · commutative algebra

MvPowerSeries.commute_monomial

∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (φ : MvPowerSeries σ R) {a : R} {n : σ →₀ ℕ},
  Commute φ ((MvPowerSeries.monomial n) a) ↔ ∀ (m : σ →₀ ℕ), Commute ((MvPowerSeries.coeff m) φ) a

Defined in

Mathlib.RingTheory.MvPowerSeries.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

Semiring