Theorems · Definition · commutative algebra

HahnSeries.single

{Γ : Type u_1} → {R : Type u_3} → [inst : PartialOrder Γ] → [inst_1 : Zero R] → Γ → ZeroHom R (HahnSeries Γ R)

single a r is the Hahn series which has coefficient r at a and zero otherwise.

Defined in

Mathlib.RingTheory.HahnSeries.Basic

Cited by

82 results in Mathlib

Foundations

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

Assumes

PartialOrderZero