int_not_isCoprime_helper

Mathlib.Tactic.NormNum.IsCoprime

URI: https://scilib.ai/kg/mathlib#Tactic.NormNum.int_not_isCoprime_helper

Lean4

theorem int_not_isCoprime_helper (x y : ℤ) (d : ℕ) (hd : Int.gcd x y = d) (h : Nat.beq d 1 = false) : ¬IsCoprime x y :=
  by
  rw [Int.isCoprime_iff_gcd_eq_one, hd]
  exact Nat.ne_of_beq_eq_false h

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

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

Разделы

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

Аффилиация

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