Theorems · Definition · commutative algebra

Valuation.RankLeOne.rankOne_of_exists

{Γ₀ : Type u_2} →
  [inst : LinearOrderedCommGroupWithZero Γ₀] →
    {K : Type u_3} →
      [inst_1 : DivisionRing K] → (v : Valuation K Γ₀) → [v.RankLeOne] → (∃ x, x ≠ 0 ∧ v x ≠ 1) → v.RankOne

If a valuation has rank at most one and is non trivial, then it has rank one

Defined in

Mathlib.RingTheory.Valuation.RankOne

Cited by

0 results in Mathlib

Foundations

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

Assumes

LinearOrderedCommGroupWithZeroDivisionRingValuation.RankLeOne