Documentation

Mathlib.RingTheory.MvPowerSeries.LexOrder

LexOrder of multivariate power series #

Given an ordering of σ such that WellFoundedGT σ, 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.

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
    @[simp]
    theorem MvPowerSeries.lexOrder_zero {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] :
    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) :
    (coeff 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) :
    (coeff 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 : (coeff 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 → (coeff d) φ = 0
    source
    theorem MvPowerSeries.min_lexOrder_le {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] {φ ψ : 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} {p q : σ →₀ ℕ} (hp : φ.lexOrder = ↑(toLex p)) (hq : ψ.lexOrder = ↑(toLex q)) :
    (coeff (p + q)) (φ * ψ) = (coeff p) φ * (coeff q) ψ
    source
    theorem MvPowerSeries.le_lexOrder_mul {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] (φ ψ : MvPowerSeries σ R) :
    φ.lexOrder + ψ.lexOrder ≤ (φ * ψ).lexOrder
    source
    theorem MvPowerSeries.lexOrder_mul_ge {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] (φ ψ : 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) :
    (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder