subset_span_setGcd

Mathlib.NumberTheory.FrobeniusNumber

URI: https://scilib.ai/kg/mathlib#Nat.subset_span_setGcd

English

For any s, every element of s lies in the ideal generated by setGcd(s).

Русский

Для любого s каждый элемент множества принадлежит идеалу, порождаемому setGcd(s).

LaTeX

$$$s \\subseteq \\mathrm{Ideal.span}\\{\\mathrm{setGcd}(s)\\}$$$

Lean4

theorem subset_span_setGcd : s ⊆ Ideal.span {setGcd s} := fun _x hx ↦
  Ideal.mem_span_singleton.mpr (setGcd_dvd_of_mem hx)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru