Theorems · Definition · commutative algebra

PreTilt.valAux

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

The valuation Perfection(O/(p)) → ℝ≥0 as a function. 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

7 results in Mathlib

Foundations

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

Assumes

FieldCommRingAlgebraFactFact