English
For any φ, ψ in MvPowerSeries, the minimum of their lex orders is ≤ lexOrder of φ + ψ.
Русский
Для любых φ, ψ в MvPowerSeries минимум лексических порядков ≤ лексПорядок φ + ψ.
LaTeX
$$theorem min_lexOrder_le {φ ψ : MvPowerSeries σ R} : min (lexOrder φ) (lexOrder ψ) ≤ lexOrder (φ + ψ)$$
Lean4
theorem lexOrder_mul [NoZeroDivisors R] (φ ψ : MvPowerSeries σ R) : lexOrder (φ * ψ) = lexOrder φ + lexOrder ψ :=
by
by_cases hφ : φ = 0
· simp only [hφ, zero_mul, lexOrder_zero, top_add]
by_cases hψ : ψ = 0
· simp only [hψ, mul_zero, lexOrder_zero, add_top]
rcases exists_finsupp_eq_lexOrder_of_ne_zero hφ with ⟨p, hp⟩
rcases exists_finsupp_eq_lexOrder_of_ne_zero hψ with ⟨q, hq⟩
apply le_antisymm _ (lexOrder_mul_ge φ ψ)
rw [hp, hq]
apply lexOrder_le_of_coeff_ne_zero (d := p + q)
rw [coeff_mul_of_add_lexOrder hp hq, mul_ne_zero_iff]
exact ⟨coeff_ne_zero_of_lexOrder hp.symm, coeff_ne_zero_of_lexOrder hq.symm⟩
