Expanded

Mathlib.Tactic.LinearCombination'

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

Lean4

/-- Result of `expandLinearCombo`, either an equality proof or a value. -/
inductive Expanded/-- A proof of `a = b`. -/

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

  | const (c : Syntax.Term)

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

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

Разделы

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

Аффилиация

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