English
The same five conditions are equivalent; this restates the TFAE for Valuation Ring context.
Русский
Та же пять условий эквивалентны друг другу; повторение теоремы о TFAE в контексте валюационного кольца.
LaTeX
$$$\\text{TFAE}(R) :\\; \\text{ValuationRing } R \\iff \\text{(к остальным условиям)}$$$
Lean4
protected theorem TFAE (R : Type u) [CommRing R] [IsDomain R] :
List.TFAE
[ValuationRing R, ∀ x : FractionRing R, IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
IsTotal R (· ∣ ·), IsTotal (Ideal R) (· ≤ ·), IsLocalRing R ∧ IsBezout R] :=
by
tfae_have 1 ↔ 2 := iff_isInteger_or_isInteger R _
tfae_have 1 ↔ 3 := iff_dvd_total
tfae_have 1 ↔ 4 := iff_ideal_total
tfae_have 1 ↔ 5 := iff_local_bezout_domain
tfae_finish
