Mathlib Map

Theorems · Theorem · commutative algebra

HahnSeries.leadingCoeff_add_eq_left

∀ {R : Type u_3} [inst : AddMonoid R] {Γ : Type u_8} [inst_1 : LinearOrder Γ] {x y : HahnSeries Γ R},
  x.orderTop < y.orderTop → (x + y).leadingCoeff = x.leadingCoeff
Defined in
Mathlib.RingTheory.HahnSeries.Addition
Cited by
3 results in Mathlib
Foundations
Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddMonoidLinearOrder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

HahnSeries.orderTop_self_sub_one_pos_iff · cited by 2HahnSeries.orderTop_self_…HahnSeries.leadingCoeff_sub · cited by 0HahnSeries.leadingCoeff_s…HahnSeries.leadingCoeff_add_eq_right · cited by 0HahnSeries.leadingCoeff_a…LinearOrder · cited by 8572LinearOrderWithTop · cited by 3754WithTopAddMonoid · cited by 2864AddMonoidadd_zero · cited by 2707add_zeroHahnSeries · cited by 528HahnSeriesHahnSeries.coeff · cited by 235HahnSeries.coeffHahnSeries.orderTop · cited by 103HahnSeries.orderTopHahnSeries.leadingCoeff · cited by 49HahnSeries.leadingCoeffWithTop.untop · cited by 36WithTop.untopLT.lt.ne_top · cited by 34lt.ne_topHahnSeries.orderTop_zero · cited by 22HahnSeries.orderTop_zeroWithTop.coe_untop · cited by 17WithTop.coe_untopHahnSeries.orderTop_ne_top · cited by 13HahnSeries.orderTop_ne_topHahnSeries.leadingCoeff_of_ne_zero · cited by 11HahnSeries.leadingCoeff_o…HahnSeries.coeff_eq_zero_of_lt_orderTop · cited by 9HahnSeries.coeff_eq_zero_…HahnSeries.leadingCoeff_add_e…CITED BYCITES

Cites18

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

Cited by3

Results whose statement or proof uses this declaration.