order_smul_not_lt — Mathlib

English

For Hahn series, if r•x ≠ 0, then (r•x).order does not lie below x.order in the linear order.

Русский

Для Hahn-рядов, если r•x ≠ 0, то (r•x).order не меньше order x в порядке.

LaTeX

$$$$ \forall r,x,\; r\cdot x \neq 0 \Rightarrow (r\cdot x).order \ge x.order. $$$$

Lean4

theorem order_smul_not_lt [Zero Γ] (r : R) (x : HahnSeries Γ V) (h : r • x ≠ 0) : ¬(r • x).order < x.order :=
  by
  have hx : x ≠ 0 := right_ne_zero_of_smul h
  simp_all only [order, dite_false]
  exact Set.IsWF.min_of_subset_not_lt_min (Function.support_smul_subset_right (fun _ => r) x.coeff)

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