Theorems · Theorem · commutative algebra
HahnSeries.order_le_of_coeff_ne_zero
∀ {R : Type u_3} [inst : Zero R] {Γ : Type u_5} [inst_1 : Zero Γ] [inst_2 : LinearOrder Γ] {x : HahnSeries Γ R} {g : Γ},
x.coeff g ≠ 0 → x.order ≤ g- 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
- ZeroZeroLinearOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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
- le_transproof · cited by 985
- HahnSeriesstatement and proof · cited by 528
- le_of_eqproof · cited by 366
- HahnSeries.coeffstatement and proof · cited by 235
- HahnSeries.orderstatement · cited by 52
- HahnSeries.isWF_supportproof · cited by 33
- HahnSeries.support_nonempty_iffproof · cited by 28
- Set.IsWF.min_leproof · cited by 14
- HahnSeries.order_of_neproof · cited by 13
- HahnSeries.mem_supportproof · cited by 10
- HahnSeries.ne_zero_of_coeff_ne_zeroproof · cited by 3
Cited by6
Results whose statement or proof uses this declaration.
- HahnSeries.order_mul_of_ne_zeroproof · cited by 3
- LaurentSeries.single_order_mul_powerSeriesPartproof · cited by 3
- HahnSeries.orderTop_mul_of_ne_zeroproof · cited by 2
- HahnSeries.SummableFamily.isPWO_iUnion_support_powersproof · cited by 1
- HahnSeries.order_mulproof · cited by 1
- HahnSeries.SummableFamily.pow_finite_co_supportproof · cited by 0