leadingCoeff_neg_iff — Mathlib

English

The leading coefficient is negative exactly when the element is negative.

Русский

Ведущий коэффициент отрицателен тогда и только тогда, когда сам элемент отрицателен.

LaTeX

$${ x : Lex (HahnSeries Γ R) } \\; (ofLex x).\\mathrm{leadingCoeff} < 0 \\iff x < 0$$

Lean4

theorem leadingCoeff_neg_iff {x : Lex (HahnSeries Γ R)} : (ofLex x).leadingCoeff < 0 ↔ x < 0 := by
  simpa using (leadingCoeff_nonneg_iff (x := x)).not

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