Expanded

Mathlib.Tactic.LinearCombination

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.LinearCombination.Expanded

Lean4

/-- Result of `expandLinearCombo`, either an equality/inequality proof or a value. -/
inductive Expanded/-- A proof of `a = b`, `a ≤ b`, or `a < b` (according to the value of `Ineq`). -/

  | proof (rel : Ineq) (pf : Syntax.Term)/-- A value, equivalently a proof of `c = c`. -/

  | const (c : Syntax.Term)

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

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

Разделы

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

Аффилиация

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