Theorems · Inductive type · commutative algebra

HahnSeries

(Γ : Type u_1) → (R : Type u_2) → [PartialOrder Γ] → [Zero R] → Type (max u_1 u_2)

If Γ is linearly ordered and R has zero, then R⟦Γ⟧ consists of formal series over Γ with coefficients in R, whose supports are well-founded.

Defined in

Mathlib.RingTheory.HahnSeries.Basic

Cited by

528 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

PartialOrderZero