gcd_mono — Mathlib

English

If s1 and s2 are finite subsets with s1 ⊆ s2, then the gcd of f over s2 divides the gcd of f over s1.

Русский

Если s1 и s2 — конечные подмножества, и s1 ⊆ s2, то НОД (f) над s2 делится на НОД (f) над s1.

LaTeX

$$$\\forall \\{s_1 s_2 : \\mathrm{Finset}\\, \\beta\\} \\{f : \\beta \\to \\alpha\\},\, s_1 \\subseteq s_2 \\Rightarrow (s_2.gcd f) \\mid (s_1.gcd f)$$$

Lean4

theorem gcd_mono (h : s₁ ⊆ s₂) : s₂.gcd f ∣ s₁.gcd f :=
  dvd_gcd fun _ hb ↦ gcd_dvd (h hb)

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