le_total_ideal — Mathlib

English

In a valuation ring, the ideals are totally ordered by inclusion.

Русский

В валюационном кольце идеалы образуют полную линейную цепь по включению.

LaTeX

$$$ \\forall I,J \\in \\mathrm{Ideal}(A),\\ I \\le J \\lor J \\le I $$$

Lean4

instance le_total_ideal : IsTotal (Ideal A) LE.le := by
  constructor; intro α β
  by_cases h : α ≤ β; · exact Or.inl h
  rw [SetLike.le_def, not_forall] at h
  push_neg at h
  obtain ⟨a, h₁, h₂⟩ := h
  right
  intro b hb
  obtain ⟨c, h | h⟩ := PreValuationRing.cond a b
  · rw [← h]
    exact Ideal.mul_mem_right _ _ h₁
  · exfalso; apply h₂; rw [← h]
    apply Ideal.mul_mem_right _ _ hb

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