gcd_mono

Mathlib.Algebra.GCDMonoid.Multiset

URI: https://scilib.ai/kg/mathlib#Multiset.gcd_mono

English

If s1 ⊆ s2, then gcd(s2) divides gcd(s1).

Русский

Если s1 ⊆ s2, тогда gcd(s2) делит gcd(s1).

LaTeX

$$$s_1 \subseteq s_2 \Rightarrow s_2.\mathrm{gcd} \mid s_1.\mathrm{gcd}$$$

Lean4

theorem gcd_mono {s₁ s₂ : Multiset α} (h : s₁ ⊆ s₂) : s₂.gcd ∣ s₁.gcd :=
  dvd_gcd.2 fun _ hb ↦ gcd_dvd (h hb)

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

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

Разделы

Аффилиация

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