setGcd_dvd_of_mem_closure

Mathlib.NumberTheory.FrobeniusNumber

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

← MathLib Explorer

English

If n belongs to the additive closure of s, then setGcd(s) divides n.

Русский

Если n ∈ замыкание_сложения(s), то setGcd(s) делит n.

LaTeX

$$$n \\in \\mathrm{AddSubmonoid.closure}(s) \\Rightarrow \\mathrm{setGcd}(s) \\mid n$$$

Lean4

theorem setGcd_dvd_of_mem_closure (h : n ∈ AddSubmonoid.closure s) : setGcd s ∣ n :=
  AddSubmonoid.closure_induction (fun _ ↦ setGcd_dvd_of_mem) (dvd_zero _) (fun _ _ _ _ ↦ dvd_add) h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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