isNNRat

Mathlib.Tactic.NormNum.Result

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.NormNum.Result.isNNRat

Lean4

/-- The result is `proof : IsNNRat x n d`,
where `n` a raw nat literal, `d` is a raw nat literal (not 0 or 1),
`n` and `d` are coprime, and `q` is the value of `n / d`. -/
@[match_pattern, inline]
def isNNRat {α : Q(Type u)} {x : Q($α)} :
    ∀ (inst : Q(DivisionSemiring $α) := by assumption) (q : Rat) (n : Q(ℕ)) (d : Q(ℕ)) (proof : Q(IsNNRat $x $n $d)),
      Result x :=
  Result'.isNNRat

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

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

Разделы

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

Аффилиация

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