English
The leading coefficient of the absolute value equals the absolute value of the leading coefficient.
Русский
Ведущий коэффициент модуля равен модулю ведущего коэффициента.
LaTeX
$$$ (\\mathrm{ofLex} (|x|)).\\mathrm{leadingCoeff} = |(\\mathrm{ofLex} x).\\mathrm{leadingCoeff}| $$$
Lean4
theorem leadingCoeff_abs (x : Lex (HahnSeries Γ R)) : (ofLex |x|).leadingCoeff = |(ofLex x).leadingCoeff| :=
by
obtain hlt | rfl | hgt := lt_trichotomy x 0
· obtain hlt' := leadingCoeff_neg_iff.mpr hlt
rw [abs_eq_neg_self.mpr hlt.le, abs_eq_neg_self.mpr hlt'.le, ofLex_neg, leadingCoeff_neg]
· simp
· obtain hgt' := leadingCoeff_pos_iff.mpr hgt
rw [abs_eq_self.mpr hgt.le, abs_eq_self.mpr hgt'.le]