English
For any x in Lex(HahnSeries Γ R), the sign of the leading coefficient of ofLex x reflects the sign of x: 0 < (ofLex x).leadingCoeff iff 0 < x.
Русский
Для любого x в Lex(HahnSeries Γ R) знак ведущего коэффициента отражает знак x: 0 < leadingCoeff(ofLex x) тогда и только тогда, когда 0 < x.
LaTeX
$${ x : Lex (HahnSeries Γ R) } \\; 0 < (\\mathrm{ofLex} x).\\mathrm{leadingCoeff} \\iff 0 < x$$
Lean4
@[simp]
theorem leadingCoeff_pos_iff {x : Lex (HahnSeries Γ R)} : 0 < (ofLex x).leadingCoeff ↔ 0 < x :=
by
rw [lt_iff]
constructor
· intro hpos
have hne : (ofLex x) ≠ 0 := leadingCoeff_ne_zero.mp hpos.ne.symm
have htop : (ofLex x).orderTop ≠ ⊤ := orderTop_ne_top.2 hne
refine ⟨(ofLex x).orderTop.untop htop, ?_, by simpa [coeff_untop_eq_leadingCoeff] using hpos⟩
intro j hj
simpa using (coeff_eq_zero_of_lt_orderTop ((WithTop.lt_untop_iff htop).mp hj)).symm
· intro ⟨i, hj, hi⟩
have horder : (ofLex x).orderTop = WithTop.some i :=
by
apply orderTop_eq_of_le
· simpa using hi.ne.symm
· intro g hg
contrapose! hg
simpa using (hj g hg).symm
have htop : (ofLex x).orderTop ≠ ⊤ := WithTop.ne_top_iff_exists.mpr ⟨i, horder.symm⟩
have hne : ofLex x ≠ 0 := orderTop_ne_top.1 htop
have horder' : (ofLex x).orderTop.untop htop = i := (WithTop.untop_eq_iff _).mpr horder
rw [leadingCoeff_of_ne_zero hne, horder']
simpa using hi
