iff_ideal_total — Mathlib

English

A PreValuationRing R is equivalent to IsTotal(Ideal R, ≤).

Русский

Предвалюационное кольцо R эквивалентно тому, что множество идеалов упорядовано по включению (≤) в целом.

LaTeX

$$$\\text{PreValuationRing } R \\iff \\mathrm{IsTotal}(\\mathrm{Ideal} R)(\\le)$$$

Lean4

theorem _root_.PreValuationRing.iff_ideal_total [CommRing R] : PreValuationRing R ↔ IsTotal (Ideal R) (· ≤ ·) := by
  classical
  refine ⟨fun _ => ⟨le_total⟩, fun H => PreValuationRing.iff_dvd_total.mpr ⟨fun a b => ?_⟩⟩
  have := @IsTotal.total _ _ H (Ideal.span { a }) (Ideal.span { b })
  simp_rw [Ideal.span_singleton_le_span_singleton] at this
  exact this.symm

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