Theorems · Definition · commutative algebra

PowerSeries.substAlgHom

{R : Type u_2} →
  [inst : CommRing R] →
    {τ : Type u_3} →
      {S : Type u_4} →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            {a : MvPowerSeries τ S} → PowerSeries.HasSubst a → PowerSeries R →ₐ[R] MvPowerSeries τ S

Substitution of power series into a power series, as an AlgHom.

Defined in

Mathlib.RingTheory.PowerSeries.Substitution

Cited by

16 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra