cancelDenoms

Mathlib.Tactic.Linarith.Preprocessing

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Linarith.cancelDenoms

Lean4

/-- `cancelDenoms pf` assumes `pf` is a proof of `t R 0`. If `t` contains the division symbol `/`,
it tries to scale `t` to cancel out division by numerals.
-/
def cancelDenoms : Preprocessor where
  description := "cancel denominators"
  transform := fun pf =>
    (do
        let (_, lhs) ← parseCompAndExpr (← inferType pf)
        guard <|
            lhs.containsConst <| fun n =>
              n = ``HDiv.hDiv || n = ``Div.div || n = ``Inv.inv || n == ``OfScientific.ofScientific
        pure [← normalizeDenominatorsLHS pf lhs]) <|>
      return [pf]

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

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

Разделы

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

Аффилиация

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