Mathlib Map

Theorems · Theorem · commutative algebra

HahnSeries.order_one

∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero Γ] [inst_1 : PartialOrder Γ] [inst_2 : MulZeroOneClass R],
  HahnSeries.order 1 = 0
Defined in
Mathlib.RingTheory.HahnSeries.Multiplication
Cited by
2 results in Mathlib
Foundations
Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
ZeroPartialOrderMulZeroOneClass
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

HahnSeries.leadingCoeff_one · cited by 1HahnSeries.leadingCoeff_o…HahnSeries.isUnit_iff · cited by 0HahnSeries.isUnit_iffPartialOrder · cited by 6410PartialOrderNontrivial · cited by 2416Nontrivialone_ne_zero · cited by 885one_ne_zeroHahnSeries · cited by 528HahnSeriesMulZeroOneClass · cited by 184MulZeroOneClasssubsingleton_or_nontrivial · cited by 161subsingleton_or_nontrivialHahnSeries.order · cited by 52HahnSeries.orderHahnSeries.order_zero · cited by 11HahnSeries.order_zeroHahnSeries.order_single · cited by 4HahnSeries.order_singleHahnSeries.order_oneCITED BYCITES

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.