evenToNeg_comp_evenToNeg — Mathlib

English

The EvenToNeg map respects the action on generators in a graded fashion; specifically, the action on (even.ι Q).bilin by evenToNeg is the negative of the corresponding bilinear form in Q'.

Русский

Операция EvenToNeg корректно действует на генераторы; на элементе (even.ι Q).bilin отображение даёт отрицание соответствующей bilinear-формы в Q'.

LaTeX

$$$ evenToNeg Q Q' h ((even.ι Q).bilin m_1 m_2) = - (even.ι Q').bilin m_1 m_2 $$$

Lean4

theorem evenToNeg_comp_evenToNeg (Q' : QuadraticForm R M) (h : Q' = -Q) (h' : Q = -Q') :
    (evenToNeg Q' Q h').comp (evenToNeg Q Q' h) = AlgHom.id R _ :=
  by
  ext m₁ m₂ : 4
  simp [evenToNeg_ι]

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