valuationSubring_not_isField — Mathlib

English

If the value group is nontrivial and cyclic, the valuation subring is not a field.

Русский

Если группа значений ненулевая и циклична, то подкольцо оценки не является полем.

LaTeX

$$$\neg \operatorname{IsField}(v.valuationSubring).$$$

Lean4

theorem valuationSubring_not_isField [Nontrivial ↥(valueGroup v)] [IsCyclic (valueGroup v)] : ¬IsField K₀ :=
  by
  obtain ⟨π, hπ⟩ := exists_isUniformizer_of_isCyclic_of_nontrivial v
  rintro ⟨-, -, h⟩
  have := hπ.ne_zero
  simp only [ne_eq, Subring.coe_eq_zero_iff] at this
  specialize h this
  rw [← isUnit_iff_exists_inv] at h
  exact hπ.not_isUnit h

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