isRankOneDiscrete — Mathlib

English

For a DVR A and a field K, the valuation v = maximalIdeal A.valuation K is rank-one discrete.

Русский

Для дискриминированного DVR A и поля K оценка, связанная с максимальным идеалом, имеет ранг один и дискретность.

LaTeX

$$$ IsRankOneDiscrete\\ ((\\maximalIdeal A).valuation\\ K). $$$

Lean4

instance isRankOneDiscrete : IsRankOneDiscrete ((maximalIdeal A).valuation K) :=
  by
  have : Nontrivial ↥(valueGroup (valuation K (maximalIdeal A))) :=
    by
    let v := (maximalIdeal A).valuation K
    let π := valuation_exists_uniformizer K (maximalIdeal A) |>.choose
    have hπ : v π = ↑(ofAdd (-1 : ℤ)) := valuation_exists_uniformizer K (maximalIdeal A) |>.choose_spec
    rw [Subgroup.nontrivial_iff_exists_ne_one]
    use Units.mk0 (v π) (by simp [hπ])
    constructor
    · apply mem_valueGroup
      simp only [Units.val_mk0, Set.mem_range]
      use π
    · simpa [hπ] using not_eq_of_beq_eq_false rfl
  infer_instance

Похожие утверждения