Theorems · Inductive type · commutative algebra

Valuation.RankOne

{R : Type u_1} →
  {Γ₀ : Type u_2} → [inst : Ring R] → [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → Valuation R Γ₀ → Type u_2

A valuation has rank one if it is nontrivial and its image is contained in ℝ≥0. Note that this class includes the data of an inclusion morphism Γ₀ → ℝ≥0.

Defined in

Mathlib.RingTheory.Valuation.RankOne

Cited by

32 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

RingLinearOrderedCommGroupWithZero