rearrangeData

Mathlib.Tactic.LinearCombination.Lemmas

URI: https://scilib.ai/kg/mathlib#Mathlib.Ineq.rearrangeData

Lean4

/-- Given an (in)equality, look up the lemma to move everything to the LHS. -/
def rearrangeData : Ineq → Name
  | eq => ``eq_rearrange
  | le => ``le_rearrange
  | lt => ``lt_rearrange

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

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

Разделы

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

Аффилиация

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