gcd_union — Mathlib

English

The gcd over the union equals the gcd of gcds over each set: gcd(s1 ∪ s2, f) = gcd(gcd(s1,f), gcd(s2,f)).

Русский

НОД по объединению равен НОД двух НОД по отдельным множествам.

LaTeX

$$$ (s_1 \cup s_2).gcd f = \operatorname{gcd}( s_1.gcd f, s_2.gcd f )$$$

Lean4

theorem gcd_union [DecidableEq β] : (s₁ ∪ s₂).gcd f = GCDMonoid.gcd (s₁.gcd f) (s₂.gcd f) :=
  Finset.induction_on s₁ (by rw [empty_union, gcd_empty, gcd_zero_left, normalize_gcd]) fun a s _ ih ↦ by
    rw [insert_union, gcd_insert, gcd_insert, ih, gcd_assoc]

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