Theorems · Theorem · commutative algebra

MvPowerSeries.rename_rename

∀ {σ : Type u_1} {τ : Type u_2} {γ : Type u_3} {R : Type u_4} (f : σ → τ) (g : τ → γ) [inst : Filter.TendstoCofinite f]
  [inst_1 : CommSemiring R] [inst_2 : Filter.TendstoCofinite g] (p : MvPowerSeries σ R),
  (MvPowerSeries.rename g) ((MvPowerSeries.rename f) p) = (MvPowerSeries.rename (g ∘ f)) p

Defined in

Mathlib.RingTheory.MvPowerSeries.Rename

Cited by

3 results in Mathlib

Foundations

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

Assumes

Filter.TendstoCofiniteCommSemiringFilter.TendstoCofinite