Theorems · Definition · commutative algebra

ModP.preVal

(K : Type u₁) →
  [inst : Field K] →
    Valuation K NNReal → (O : Type u₂) → [inst_1 : CommRing O] → [Algebra O K] → (p : ℕ) → ModP O p → NNReal

For a field K with valuation v : K → ℝ≥0 and ring of integers O, a function O/(p) → ℝ≥0 that sends 0 to 0 and x + (p) to v(x) as long as x ∉ (p).

Defined in

Mathlib.RingTheory.Perfection

Cited by

11 results in Mathlib

Foundations

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

Assumes

FieldCommRingAlgebra