Theorems · Theorem · commutative algebra

HahnSeries.orderTop_single

∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {a : Γ} {r : R},
  r ≠ 0 → ((HahnSeries.single a) r).orderTop = ↑a

Defined in

Mathlib.RingTheory.HahnSeries.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

PartialOrderZero