Theorems · Theorem · commutative algebra

HahnSeries.map_coeff

∀ {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero S]
  (x : HahnSeries Γ R) {F : Type u_5} [inst_3 : FunLike F R S] [inst_4 : ZeroHomClass F R S] (f : F) (g : Γ),
  (x.map f).coeff g = f (x.coeff g)

Defined in

Mathlib.RingTheory.HahnSeries.Basic

Cited by

8 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext

Assumes

PartialOrderZeroZeroFunLikeZeroHomClass