Theorems · Definition · commutative algebra

Valuation.IsRankOneDiscrete.generator

{Γ : Type u_1} →
  [inst : LinearOrderedCommGroupWithZero Γ] →
    {A : Type u_2} → [inst_1 : Ring A] → (v : Valuation A Γ) → [v.IsRankOneDiscrete] → Γˣ

Given a discrete valuation v, Valuation.IsRankOneDiscrete.generator is an element of Γ which is a generator of the value group that is < 1.

Defined in

Mathlib.RingTheory.Valuation.Discrete.Basic

Cited by

24 results in Mathlib

Foundations

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

Assumes

LinearOrderedCommGroupWithZeroRingValuation.IsRankOneDiscrete