Theorems · Definition · commutative algebra

HahnSeries.map

{Γ : Type u_1} →
  {R : Type u_3} →
    {S : Type u_4} →
      [inst : PartialOrder Γ] →
        [inst_1 : Zero R] →
          [inst_2 : Zero S] →
            HahnSeries Γ R → {F : Type u_5} → [inst_3 : FunLike F R S] → [ZeroHomClass F R S] → F → HahnSeries Γ S

The map of Hahn series induced by applying a zero-preserving map to each coefficient.

Defined in

Mathlib.RingTheory.HahnSeries.Basic

Cited by

13 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext

Assumes

PartialOrderZeroZeroFunLikeZeroHomClass