span_singleton_setGcd — Mathlib

English

The ideal generated by the gcd of s over the integers equals the ideal generated by the image of s in ℤ.

Русский

ideal, порождаемый gcd s над целыми числами, равен идеалу, порождаемому изображением s в \\mathbb{Z}.

LaTeX

$$$\\mathrm{Ideal.span}\\{\\mathrm{setGcd}(s)\\} = \\mathrm{Ideal.span}\\big( ((\\uparrow) : \\mathbb{N} \\to \\mathbb{Z}) '' s \\big)$$$

Lean4

theorem span_singleton_setGcd : Ideal.span {(setGcd s : ℤ)} = Ideal.span (((↑) : ℕ → ℤ) '' s) := by
  rw [setGcd, ← Ideal.span_singleton_eq_span_singleton.mpr (Int.associated_natAbs _), Ideal.span,
    span_singleton_generator]

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