Theorems · Definition · commutative algebra
HahnSeries.ofSuppBddBelow
{Γ : Type u_1} →
{R : Type u_3} →
[inst : Zero R] →
[inst_1 : LinearOrder Γ] → [LocallyFiniteOrder Γ] → (f : Γ → R) → BddBelow (Function.support f) → HahnSeries Γ RConstruct a Hahn series from any function whose support is bounded below.
- Defined in
- Mathlib.RingTheory.HahnSeries.Basic
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LinearOrderstatement and proof · cited by 8,572
- LocallyFiniteOrderstatement and proof · cited by 658
- Function.supportstatement and proof · cited by 610
- HahnSeriesstatement · cited by 528
- BddBelowstatement and proof · cited by 401
Cited by8
Results whose statement or proof uses this declaration.
- LaurentSeries.hasseDerivproof · cited by 9
- HahnSeries.ofSuppBddBelow_zerostatement · cited by 1
- HahnSeries.ofSuppBddBelow.congr_simpstatement and proof · cited by 0
- HahnSeries.order_ofForallLtEqZerostatement · cited by 0
- HahnSeries.zero_ofSuppBddBelowstatement · cited by 0
- HahnSeries.coeff_ofSuppBddBelowstatement · cited by 0
- HahnSeries.ofSuppBddBelow_coeffstatement and proof · cited by 0
- HahnSeries.ofSuppBddBelow_eq_zerostatement · cited by 0