expr

Mathlib.Tactic.FieldSimp.Lemmas

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.FieldSimp.Sign.expr

Lean4

/-- Given an expression `e : Q($M)`, construct an expression which is morally "± `e`", with the
choice between + and - determined by an object `g : Sign M`. -/
def expr : Sign M → Q($M) → Q($M)
  | plus, a => a
  | minus _, a => q(-$a)

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

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

Разделы

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

Аффилиация

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