gcd_insert — Mathlib

English

The gcd over insert b s equals gcd(f(b)) with gcd over s.

Русский

НОД над добавлением b к s равен НОД между f(b) и НОД над s.

LaTeX

$$$(\mathrm{insert}\ b\ s).gcd f = \gcd( f(b), s.gcd f )$$$

Lean4

@[simp]
theorem gcd_insert [DecidableEq β] {b : β} : (insert b s : Finset β).gcd f = GCDMonoid.gcd (f b) (s.gcd f) :=
  by
  by_cases h : b ∈ s
  · rw [insert_eq_of_mem h, (gcd_eq_right_iff (f b) (s.gcd f) (Multiset.normalize_gcd (s.1.map f))).2 (gcd_dvd h)]
  apply fold_insert h

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