iff_dvd_total — Mathlib

English

For any semigroup R, PreValuationRing R is equivalent to IsTotal R (x ∣ y).

Русский

Для любого полугруппового множества R предвалюационная структура эквивалентна тому, что отношение делимости x ∣ y является сравнимым (полным).

LaTeX

$$$[\\Semigroup R] \\Rightarrow (\\text{PreValuationRing } R \\iff \\mathrm{IsTotal}\\ R(\\cdot \\mid \\cdot))$$$

Lean4

theorem _root_.PreValuationRing.iff_dvd_total [Semigroup R] : PreValuationRing R ↔ IsTotal R (· ∣ ·) := by
  classical
  refine ⟨fun H => ⟨fun a b => ?_⟩, fun H => ⟨fun a b => ?_⟩⟩
  · obtain ⟨c, rfl | rfl⟩ := PreValuationRing.cond a b <;> simp
  · obtain ⟨c, rfl⟩ | ⟨c, rfl⟩ := @IsTotal.total _ _ H a b <;> use c <;> simp

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