Theorems · Theorem · commutative algebra

MvPowerSeries.LinearTopology.basis_le_iff

∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] {J K : TwoSidedIdeal R} {d e : σ →₀ ℕ},
  K ≠ ⊤ →
    (MvPowerSeries.LinearTopology.basis σ R (J, d) ≤ MvPowerSeries.LinearTopology.basis σ R (K, e) ↔ J ≤ K ∧ e ≤ d)

basis σ R ⟨J, d⟩ ≤ basis σ R ⟨K, e⟩ if and only if J ≤ K and e ≤ d.

Defined in

Mathlib.RingTheory.MvPowerSeries.LinearTopology

Cited by

0 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Ring