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⟩