neg_proof — Mathlib

English

The quadratic map associated to the negation of B equals Q − Q′ when h relates B to Q′ − Q.

Русский

Квадратичная карта, ассоциированная со знаком минус B, равна Q − Q′ при условии, что h связывает B с Q′ − Q.

LaTeX

$$$ (-B).toQuadraticMap = Q - Q' $$$

Lean4

/-- Auxiliary lemma used as an argument to `CliffordAlgebra.changeForm` -/
theorem neg_proof : (-B).toQuadraticMap = Q - Q' :=
  (congr_arg Neg.neg h).trans <| neg_sub _ _

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