setGcd_mono

Mathlib.NumberTheory.FrobeniusNumber

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

English

If s ⊆ t then setGcd(t) divides setGcd(s).

Русский

Если s ⊆ t, тогда setGcd(t) делит setGcd(s).

LaTeX

$$$s \\subseteq t \\Rightarrow \\mathrm{setGcd}(t) \\mid \\mathrm{setGcd}(s)$$$

Lean4

theorem setGcd_mono (h : s ⊆ t) : setGcd t ∣ setGcd s :=
  dvd_setGcd_iff.mpr fun _m hm ↦ setGcd_dvd_of_mem (h hm)

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

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

Разделы

Аффилиация

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