order_single_mul_of_isRegular — Mathlib

English

Under regularity, a single-term shift scales the order additively with the base order.

Русский

При регулярности сдвиг одного терма добавляет порядок к порядку x.

LaTeX

$$$ ( (\mathrm{single}\; g\; r) * x ).order = g + x.order $$$

Lean4

theorem order_single_mul_of_isRegular {g : Γ} {r : R} (hr : IsRegular r) {x : HahnSeries Γ R} (hx : x ≠ 0) :
    (((single g) r) * x).order = g + x.order :=
  by
  obtain _ | _ := subsingleton_or_nontrivial R
  · exact (hx <| Subsingleton.eq_zero x).elim
  have hrx : ((single g) r).leadingCoeff * x.leadingCoeff ≠ 0 := by
    rwa [leadingCoeff_of_single, ne_eq, hr.left.mul_left_eq_zero_iff, leadingCoeff_eq_zero]
  rw [order_mul_of_nonzero hrx, order_single <| IsRegular.ne_zero hr]

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