iff_local_bezout_domain — Mathlib

English

A ring is a valuation ring if and only if it is local and Bézout.

Русский

Кольцо является валюационным кольцом тогда и только тогда, когда оно локальное и Bezout.

LaTeX

$$$\\text{ValuationRing } R \\iff (\\text{IsLocalRing } R \\land \\text{IsBezout } R)$$$

Lean4

theorem iff_local_bezout_domain : ValuationRing R ↔ IsLocalRing R ∧ IsBezout R :=
  ⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ inferInstance⟩

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