Theorems · Definition · commutative algebra
HahnSeries.toOrderTopSubOnePos
{Γ : Type u_1} →
{R : Type u_3} →
[inst : AddCommMonoid Γ] →
[inst_1 : LinearOrder Γ] →
[inst_2 : IsOrderedCancelAddMonoid Γ] →
[inst_3 : CommRing R] → {x : HahnSeries Γ R} → 0 < (x - 1).orderTop → ↥(HahnSeries.orderTopSubOnePos Γ R)Make an element of orderTopSubOnePos
- Defined in
- Mathlib.RingTheory.HahnSeries.Summable
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- AddCommMonoidstatement and proof · cited by 12,281
- LinearOrderstatement and proof · cited by 8,572
- WithTopstatement · cited by 3,754
- Subgroupstatement · cited by 3,593
- Unitsstatement · cited by 2,804
- HahnSeriesstatement and proof · cited by 528
- IsOrderedCancelAddMonoidstatement and proof · cited by 359
- IsUnit.unitproof · cited by 252
- HahnSeries.orderTopstatement and proof · cited by 103
- Units.invproof · cited by 35
- HahnSeries.orderTopSubOnePosstatement · cited by 7
Cited by5
Results whose statement or proof uses this declaration.
- HahnSeries.toOrderTopSubOnePos.congr_simpstatement and proof · cited by 2
- HahnSeries.val_toOrderTopSubOnePos_coestatement and proof · cited by 2
- HahnSeries.coeff_toOrderTopSubOnePos_powstatement and proof · cited by 0
- HahnSeries.val_inv_toOrderTopSubOnePos_coestatement and proof · cited by 0
- HahnSeries.binomial_powerstatement · cited by 0