inferLinearOrderedField

Mathlib.Tactic.NormNum.Ineq

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

Lean4

/-- Helper function to synthesize typed `Field α` `LinearOrder α` `IsStrictOrderedRing α`
expressions. -/
def inferLinearOrderedField (α : Q(Type u)) :
    MetaM <| (_ : Q(Field $α)) × (_ : Q(LinearOrder $α)) × Q(IsStrictOrderedRing $α) :=
  let go := do
    let field ← synthInstanceQ q(Field $α)
    let linearOrder ← synthInstanceQ q(LinearOrder $α)
    let isStrictOrderedRing ← synthInstanceQ q(IsStrictOrderedRing $α)
    return ⟨field, linearOrder, isStrictOrderedRing⟩
  go <|> throwError"not a linear ordered field"

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

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

Разделы

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

Аффилиация

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