Theorems · Inductive type · commutative algebra

Valuation.Uniformizer

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

The structure Uniformizer bundles together the term in the ring and a proof that it is a uniformizer.

Defined in: Mathlib.RingTheory.Valuation.Discrete.Basic
Cited by: 12 results in Mathlib
Foundations: Depth 3 from the axioms · uses no axioms
Assumes: LinearOrderedCommGroupWithZero Ring Valuation.IsRankOneDiscrete

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Ringstatement · cited by 7,463
Valuationstatement · cited by 823
LinearOrderedCommGroupWithZerostatement · cited by 528
Valuation.IsRankOneDiscretestatement · cited by 53

Cited by20

Results whose statement or proof uses this declaration.

Valuation.Uniformizer.valstatement and proof · cited by 10
Valuation.Uniformizer.valuation_gt_onestatement and proof · cited by 4
Valuation.Uniformizer.is_generatorstatement and proof · cited by 4
Valuation.exists_pow_Uniformizerstatement and proof · cited by 3
Valuation.ideal_isPrincipalproof · cited by 1
Valuation.Uniformizer.ne_zerostatement and proof · cited by 1
Valuation.Uniformizer.mk.injstatement · cited by 1
Valuation.Uniformizer.mk.noConfusionstatement · cited by 1
Valuation.Uniformizer.extstatement and proof · cited by 1
Valuation.Uniformizer.mk'statement · cited by 0
Valuation.Uniformizer.noConfusionstatement and proof · cited by 0
Valuation.Uniformizer.noConfusionTypestatement and proof · cited by 0