setGcd_eq_zero_iff

Mathlib.NumberTheory.FrobeniusNumber

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

← MathLib Explorer

English

setGcd(s) = 0 if and only if s ⊆ {0}.

Русский

setGcd(s) = 0 тогда и только тогда, когда s ⊆ {0}.

LaTeX

$$$\\mathrm{setGcd}(s) = 0 \\iff s \\subseteq \\{0\\}$$$

Lean4

theorem setGcd_eq_zero_iff : setGcd s = 0 ↔ s ⊆ {0} := by
  simp_rw [setGcd, Int.natAbs_eq_zero, ← eq_bot_iff_generator_eq_zero, Ideal.span_eq_bot, Set.forall_mem_image,
    Int.natCast_eq_zero, Set.subset_def, Set.mem_singleton_iff]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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