setGcd_insert_of_dvd — Mathlib

English

If setGcd(s) divides n, then setGcd(insert n s) = setGcd(s).

Русский

Если setGcd(s) делит n, то setGcd(insert n s) = setGcd(s).

LaTeX

$$$\\mathrm{setGcd}(s) \\mid n \\Rightarrow \\mathrm{setGcd}(\\mathrm{insert}(n,s)) = \\mathrm{setGcd}(s)$$$

Lean4

theorem setGcd_insert_of_dvd (h : setGcd s ∣ n) : setGcd (insert n s) = setGcd s :=
  (setGcd_mono <| Set.subset_insert ..).antisymm <|
    dvd_setGcd_iff.mpr fun m ↦ by rintro (rfl | hm); exacts [h, setGcd_dvd_of_mem hm]

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