order_mul — Mathlib

English

Let x and y be nonzero Hahn series over a well-ordered value group Γ with coefficients in a ring R (where Γ is additive, totally ordered, and cancellative). Then the order of their product equals the sum of their orders: ord(xy) = ord(x) + ord(y).

Русский

Пусть x и y — ненулевые Ханновы ряды над упорядоченной абелевой группой Γ и кольцом R; тогда порядок произведения равен сумме порядков: ord(xy) = ord(x) + ord(y).

LaTeX

$$$\\operatorname{ord}(xy) = \\operatorname{ord}(x) + \\operatorname{ord}(y) \\quad (x \\neq 0,\\; y \\neq 0).$$$

Lean4

@[simp]
theorem order_mul {Γ} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R]
    [NoZeroDivisors R] {x y : HahnSeries Γ R} (hx : x ≠ 0) (hy : y ≠ 0) : (x * y).order = x.order + y.order :=
  by
  apply le_antisymm
  · apply order_le_of_coeff_ne_zero
    rw [coeff_mul_order_add_order x y]
    exact mul_ne_zero (leadingCoeff_ne_zero.mpr hx) (leadingCoeff_ne_zero.mpr hy)
  · rw [order_of_ne hx, order_of_ne hy, order_of_ne (mul_ne_zero hx hy), ← Set.IsWF.min_add]
    exact Set.IsWF.min_le_min_of_subset support_mul_subset_add_support

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