Mathlib.RingTheory.MvPowerSeries.LexOrder

LexOrder of multivariate power series

Given an ordering of σ such that WellOrderGT σ, the lexicographic order on σ →₀ ℕ is a well ordering, which can be used to define a natural valuation lexOrder on the ring MvPowerSeries σ R: the smallest exponent in the support.

source

noncomputable def MvPowerSeries.lexOrder {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] (φ : MvPowerSeries σ R) :

WithTop (Lex (σ →₀ ℕ))

The lex order on multivariate power series.

Equations

φ.lexOrder = if h : φ = 0 then ⊤ else let_fun ne := ⋯; ↑(⋯.min (⇑toLex '' Function.support φ) ne)

Instances For

source

theorem MvPowerSeries.lexOrder_def_of_ne_zero {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] {φ : MvPowerSeries σ R} (hφ : φ ≠ 0) :

∃ (ne : (⇑toLex '' Function.support φ).Nonempty), φ.lexOrder = ↑(⋯.min (⇑toLex '' Function.support φ) ne)

source

@[simp]

theorem MvPowerSeries.lexOrder_eq_top_iff_eq_zero {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] (φ : MvPowerSeries σ R) :

φ.lexOrder = ⊤ ↔ φ = 0

source

theorem MvPowerSeries.lexOrder_zero {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] :

MvPowerSeries.lexOrder 0 = ⊤

source

theorem MvPowerSeries.exists_finsupp_eq_lexOrder_of_ne_zero {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] {φ : MvPowerSeries σ R} (hφ : φ ≠ 0) :

∃ (d : σ →₀ ℕ), φ.lexOrder = ↑(toLex d)

source

theorem MvPowerSeries.coeff_ne_zero_of_lexOrder {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] {φ : MvPowerSeries σ R} {d : σ →₀ ℕ} (h : ↑(toLex d) = φ.lexOrder) :

(MvPowerSeries.coeff R d) φ ≠ 0

source

theorem MvPowerSeries.coeff_eq_zero_of_lt_lexOrder {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] {φ : MvPowerSeries σ R} {d : σ →₀ ℕ} (h : ↑(toLex d) < φ.lexOrder) :

(MvPowerSeries.coeff R d) φ = 0

source

theorem MvPowerSeries.lexOrder_le_of_coeff_ne_zero {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] {φ : MvPowerSeries σ R} {d : σ →₀ ℕ} (h : (MvPowerSeries.coeff R d) φ ≠ 0) :

φ.lexOrder ≤ ↑(toLex d)

source

theorem MvPowerSeries.le_lexOrder_iff {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] {φ : MvPowerSeries σ R} {w : WithTop (Lex (σ →₀ ℕ))} :

w ≤ φ.lexOrder ↔ ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (MvPowerSeries.coeff R d) φ = 0

source

theorem MvPowerSeries.min_lexOrder_le {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] {φ : MvPowerSeries σ R} {ψ : MvPowerSeries σ R} :

min φ.lexOrder ψ.lexOrder ≤ (φ + ψ).lexOrder

source

theorem MvPowerSeries.coeff_mul_of_add_lexOrder {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] {φ : MvPowerSeries σ R} {ψ : MvPowerSeries σ R} {p : σ →₀ ℕ} {q : σ →₀ ℕ} (hp : φ.lexOrder = ↑(toLex p)) (hq : ψ.lexOrder = ↑(toLex q)) :

(MvPowerSeries.coeff R (p + q)) (φ * ψ) = (MvPowerSeries.coeff R p) φ * (MvPowerSeries.coeff R q) ψ

source

theorem MvPowerSeries.le_lexOrder_mul {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] (φ : MvPowerSeries σ R) (ψ : MvPowerSeries σ R) :

φ.lexOrder + ψ.lexOrder ≤ (φ * ψ).lexOrder

source

theorem MvPowerSeries.lexOrder_mul_ge {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] (φ : MvPowerSeries σ R) (ψ : MvPowerSeries σ R) :

φ.lexOrder + ψ.lexOrder ≤ (φ * ψ).lexOrder

Alias of MvPowerSeries.le_lexOrder_mul.

source

theorem MvPowerSeries.lexOrder_mul {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] [NoZeroDivisors R] (φ : MvPowerSeries σ R) (ψ : MvPowerSeries σ R) :

(φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder