dvd_generator_span_iff — Mathlib

English

In a Bézout domain, gcd x y is defined as a generator of the principal ideal span{x,y}.

Русский

В Bezout домене gcd x y определяется как генератор главного идеала span{x,y}.

LaTeX

$$gcd x y := generator (Ideal.span { x, y })$$

Lean4

theorem dvd_generator_span_iff {r : R} {s : Set R} [(Ideal.span s).IsPrincipal] :
    r ∣ generator (Ideal.span s) ↔ ∀ x ∈ s, r ∣ x
    where
  mp h x hx := h.trans <| (mem_iff_generator_dvd _).mp (Ideal.subset_span hx)
  mpr
    h :=
    have : (span R s).IsPrincipal := ‹_›
    span_induction h (dvd_zero _) (fun _ _ _ _ ↦ dvd_add) (fun _ _ _ ↦ (·.mul_left _)) (generator_mem _)

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