Theorems · Inductive type · commutative algebra

Valuation.IsRankOneDiscrete

{Γ : Type u_1} → [inst : LinearOrderedCommGroupWithZero Γ] → {A : Type u_2} → [inst_1 : Ring A] → Valuation A Γ → Prop

Given a linearly ordered commutative group with zero Γ such that Γˣ is nontrivial cyclic, a valuation v : A → Γ on a ring A is discrete, if genLTOne Γˣ belongs to the image. Note that the latter is equivalent to asking that 1 : ℤ belongs to the image of the corresponding additive valuation.

Defined in

Mathlib.RingTheory.Valuation.Discrete.Basic

Cited by

53 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

LinearOrderedCommGroupWithZeroRing