neg

Mathlib.Tactic.FieldSimp.Lemmas

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

Lean4

/-- Given an expression `y : Q($M)` with specified sign (either + or -), construct a proof that
the negation of (± `y`) (here taking the specified sign) is ∓ `y`. -/
def neg (iM : Q(Field $M)) (y : Q($M)) (g : Sign M) : MetaM (Σ (G : Sign M), Q(-$(g.expr y) = $(G.expr y))) := do
  match g with
  | .plus =>
    pure ⟨.minus iM, q(rfl)⟩
  | .minus _ =>
    assumeInstancesCommute
    pure ⟨.plus, q(neg_neg $y)⟩

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

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

Разделы

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

Аффилиация

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