gcd_dvd

Mathlib.Algebra.GCDMonoid.Finset

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

English

If b ∈ s, then s.gcd f divides f(b).

Русский

Если b ∈ s, то s.gcd f делит f(b).

LaTeX

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

Lean4

theorem gcd_dvd {b : β} (hb : b ∈ s) : s.gcd f ∣ f b :=
  dvd_gcd_iff.1 dvd_rfl _ hb

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

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

Разделы

Аффилиация

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