instRankOneNNRealV — Mathlib

English

The valuation on PadicAlgCl p has rank one: there exists a nontrivial value in its value group (generated by p).

Русский

Оценка на PadicAlgCl p имеет ранг единицы: существует ненулевое значение в группе значений, порождаемом p.

LaTeX

$$$$\text{RankOne}(v) \quad\text{where } v=\operatorname{PadicAlgCl}.valued(p).v.$$$$

Lean4

/-- The valuation on `PadicAlgCl p` has rank one. -/
instance : RankOne (PadicAlgCl.valued p).v
    where
  hom := MonoidWithZeroHom.id ℝ≥0
  strictMono' := strictMono_id
  exists_val_nontrivial := by
    use p
    have hp : Nat.Prime p := hp.1
    simp only [valuation_p, one_div, ne_eq, inv_eq_zero, Nat.cast_eq_zero, inv_eq_one, Nat.cast_eq_one]
    exact ⟨hp.ne_zero, hp.ne_one⟩

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