deriveThms

Mathlib.Tactic.CancelDenoms.Core

URI: https://scilib.ai/kg/mathlib#CancelDenoms.deriveThms

Lean4

/-- Theorems to get expression into a form that `findCancelFactor` and `mkProdPrf`
can more easily handle. These are important for dividing by rationals and negative integers. -/
def deriveThms : List Name :=
  [``div_div_eq_mul_div, ``div_neg]

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

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

Разделы

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

Аффилиация

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