instIsBezout — Mathlib

English

ValuationRing R is a Bézout domain: every finitely generated ideal is principal.

Русский

Валюационное кольцо R является Bezout-областью: любой конечно порожденный идеал является главной (один элемент порождает идеал).

LaTeX

$$$\\text{IsBezout } R$$$

Lean4

instance (priority := 100) [ValuationRing R] : IsBezout R := by
  classical
  rw [IsBezout.iff_span_pair_isPrincipal]
  intro x y
  rw [Ideal.span_insert]
  rcases le_total (Ideal.span { x } : Ideal R) (Ideal.span { y }) with h | h
  · rw [sup_eq_right.mpr h]; exact ⟨⟨_, rfl⟩⟩
  · rw [sup_eq_left.mpr h]; exact ⟨⟨_, rfl⟩⟩

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