leadingCoeff_abs — Mathlib

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]

Похожие утверждения