gcd_mono_fun

Mathlib.Algebra.GCDMonoid.Finset

URI: https://scilib.ai/kg/mathlib#Finset.gcd_mono_fun

English

If for all b in s we have f(b) ∣ g(b), then s.gcd f ∣ s.gcd g.

Русский

Если для всех b∈s выполняется f(b) ∣ g(b), то s.gcd f ∣ s.gcd g.

LaTeX

$$$(\forall b \in s,\ f(b) \mid g(b)) \Rightarrow s.gcd f \mid s.gcd g$$$

Lean4

theorem gcd_mono_fun {g : β → α} (h : ∀ b ∈ s, f b ∣ g b) : s.gcd f ∣ s.gcd g :=
  dvd_gcd fun b hb ↦ (gcd_dvd hb).trans (h b hb)

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

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

Разделы

Аффилиация

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