evalIntIsCoprime

Mathlib.Tactic.NormNum.IsCoprime

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

Lean4

/-- Evaluates the `IsCoprime` predicate over `ℤ`. -/
@[norm_num IsCoprime (_ : ℤ) (_ : ℤ)]
def evalIntIsCoprime : NormNumExt where
  eval {_ _}
    e := do
    let .app (.app _ (x : Q(ℤ))) (y : Q(ℤ)) ← Meta.whnfR e |
      failure
    let ⟨ex, p⟩ ← deriveInt x _
    let ⟨ey, q⟩ ← deriveInt y _
    match proveIntIsCoprime ex ey with
    | .inl pf =>
      have pf' : Q(IsCoprime $x $y) := q(isInt_isCoprime $p $q $pf)
      return .isTrue pf'
    | .inr pf =>
      have pf' : Q(¬IsCoprime $x $y) := q(isInt_not_isCoprime $p $q $pf)
      return .isFalse pf'

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

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

Разделы

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

Аффилиация

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