Theorems · Definition · commutative algebra

HahnSeries.order

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

The order of a nonzero Hahn series x is a minimal element of Γ where x has a nonzero coefficient, the order of 0 is 0.

Defined in

Mathlib.RingTheory.HahnSeries.Basic

Cited by

52 results in Mathlib

Foundations

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

Assumes

PartialOrderZeroZero