exists_ne_zero_of_setGcd_ne_zero

Mathlib.NumberTheory.FrobeniusNumber

URI: https://scilib.ai/kg/mathlib#Nat.exists_ne_zero_of_setGcd_ne_zero

English

If setGcd(s) ≠ 0 then there exists n ∈ s with n ≠ 0.

Русский

Если setGcd(s) ≠ 0, то существует n ∈ s такое что n ≠ 0.

LaTeX

$$$\\mathrm{setGcd}(s) \\neq 0 \\Rightarrow \\exists n \\in s, n \\neq 0$$$

Lean4

theorem exists_ne_zero_of_setGcd_ne_zero (hs : setGcd s ≠ 0) : ∃ n ∈ s, n ≠ 0 :=
  by
  contrapose! hs
  exact setGcd_eq_zero_iff.mpr hs

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru