dvdNotUnit_setGcd_insert — Mathlib

English

If gcd(s) does not divide n, then inserting n into s yields a gcd that is a nontrivial divisor of gcd(s).

Русский

Если gcd(с) не делит n, то добавление n в s дает новый gcd, который является нетривиальным делителем gcd(s).

LaTeX

$$$\\text{If } \\mathrm{setGcd}(s) \\nmid n, \\; \\mathrm{setGcd}(\\mathrm{insert}(n,s)) \\text{ is a nontrivial divisor of } \\mathrm{setGcd}(s).$$$

Lean4

theorem dvdNotUnit_setGcd_insert (h : ¬setGcd s ∣ n) : DvdNotUnit (setGcd (insert n s)) (setGcd s) :=
  dvdNotUnit_of_dvd_of_not_dvd (setGcd_mono <| Set.subset_insert ..) fun dvd ↦
    h <| dvd_setGcd_iff.mp dvd _ (Set.mem_insert ..)

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