Theorems · Definition · commutative algebra

HahnSeries.orderTop

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

The orderTop of a Hahn series x is a minimal element of WithTop Γ where x has a nonzero coefficient if x ≠ 0, and is ⊤ when x = 0.

Defined in

Mathlib.RingTheory.HahnSeries.Basic

Cited by

103 results in Mathlib

Foundations

Depth 96 from the axioms, rests on 1,734 definitions · uses propext, Classical.choice, Quot.sound

Assumes

PartialOrderZero