← all areas

Namespace HahnSeries 8 theorems

— 7 · HasRamBound 1

directly in HahnSeries 7

• Hahn series with rational exponents over an algebraically closed field HahnSeries.isAlgClosed_rat 0 below · cited by 19 · depth 10
• Membership in the e-ramified Puiseux subfield HahnSeries.mem_puiseuxRamSubfield_iff 0 below · cited by 20 · depth 11
• Newton–Puiseux bound: roots have exponents in tfrac1n!ℤ HahnSeries.hasRamBound_natDegree_factorial_of_isRoot 0 below · cited by 3 · depth 12
• Descent to integer exponents in the Hahn field K((t^ℚ)) HahnSeries.hasRamBound_one_of_forall_ringEquiv_apply_eq 0 below · cited by 1 · depth 13
• Constant Hahn series have ramification bound e HahnSeries.hasRamBound_C 1 below · cited by 1 · depth 14
• Natural numbers have every ramification bound in HahnSeries ℚ K HahnSeries.hasRamBound_natCast 1 below · cited by 1 · depth 14
• The term c t has ramification bound e HahnSeries.hasRamBound_single_one 1 below · cited by 1 · depth 14

HahnSeries.HasRamBound 1

• Ramification bounds are closed under addition HahnSeries.HasRamBound.add 1 below · cited by 1 · depth 14