leadingCoeff_nonpos_iff

Mathlib.RingTheory.HahnSeries.Lex

URI: https://scilib.ai/kg/mathlib#HahnSeries.leadingCoeff_nonpos_iff

English

The nonpositivity of the g leading coefficient corresponds to the nonpositivity of x.

Русский

Ненегативность ведущего коэффициента соответствует неблагоприятному знаку x.

LaTeX

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

Lean4

theorem leadingCoeff_nonpos_iff {x : Lex (HahnSeries Γ R)} : (ofLex x).leadingCoeff ≤ 0 ↔ x ≤ 0 := by simp [← not_lt]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru