isNontrivial_iff_not_a_field — Mathlib

English

A valuation v is nontrivial if and only if the maximal ideal of the valuation ring is nonzero.

Русский

Оценка непотрівна тогда и только тогда, когда максимальный идеал кольца оценки не равен нулю.

LaTeX

$$$$ v.IsNontrivial \iff \mathrm{MaximalIdeal}(\mathcal{O}_K) \neq \{0\}. $$$$

Lean4

theorem _root_.Valuation.isNontrivial_iff_not_a_field {K Γ : Type*} [Field K] [LinearOrderedCommGroupWithZero Γ]
    (v : Valuation K Γ) : v.IsNontrivial ↔ IsLocalRing.maximalIdeal v.integer ≠ ⊥ :=
  by
  simp_rw [ne_eq, eq_bot_iff, v.isNontrivial_iff_exists_lt_one, SetLike.le_def, Ideal.mem_bot, not_forall, exists_prop,
    IsLocalRing.notMem_maximalIdeal.not_right, Valuation.Integer.not_isUnit_iff_valuation_lt_one]
  exact ⟨fun ⟨x, hx0, hx1⟩ ↦ ⟨⟨x, hx1.le⟩, by simp [Subtype.ext_iff, *]⟩, fun ⟨x, hx1, hx0⟩ ↦ ⟨x, by simp [*]⟩⟩

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