Theorems · Definition · commutative algebra

PreTilt.val

(K : Type u₁) →
  [inst : Field K] →
    (v : Valuation K NNReal) →
      (O : Type u₂) →
        [inst_1 : CommRing O] →
          [inst_2 : Algebra O K] →
            v.Integers O →
              (p : ℕ) → [inst : Fact (Nat.Prime p)] → [inst_3 : Fact ¬IsUnit ↑p] → Valuation (PreTilt O p) NNReal

The valuation Perfection(O/(p)) → ℝ≥0. Given f ∈ Perfection(O/(p)), if f = 0 then output 0; otherwise output preVal(f(n))^(p^n) for any n such that f(n) ≠ 0.

Defined in

Mathlib.RingTheory.Perfection

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldCommRingAlgebraFactFact