setGcd_dvd_of_mem

Mathlib.NumberTheory.FrobeniusNumber

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

← MathLib Explorer

English

If n is in s, then setGcd(s) divides n.

Русский

Если n ∈ s, то setGcd(s) делит n.

LaTeX

$$If $n \\in s$, then $\\mathrm{setGcd}(s) \\mid n$.$$

Lean4

theorem setGcd_dvd_of_mem (h : n ∈ s) : setGcd s ∣ n :=
  by
  rw [setGcd, ← Int.dvd_natCast, ← mem_iff_generator_dvd]
  exact Ideal.subset_span ⟨n, h, rfl⟩

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

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

Разделы

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

Аффилиация

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