isInt_not_isCoprime

Mathlib.Tactic.NormNum.IsCoprime

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

Lean4

theorem isInt_not_isCoprime : {x y nx ny : ℤ} → IsInt x nx → IsInt y ny → ¬IsCoprime nx ny → ¬IsCoprime x y
  | _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, h => h

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

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

Разделы

Аффилиация

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