evenToNeg_ι — Mathlib

English

The composition of the two EvenToNeg maps along the negation chain is the identity: (evenToNeg Q' Q h').comp (evenToNeg Q Q' h) = AlgHom.id R _.

Русский

Пусть есть две карты EvenToNeg вдоль цепи отрицания; их композиция возвращает тождественное отображение: (evenToNeg Q' Q h').comp (evenToNeg Q Q' h) = идентичность.

LaTeX

$$$ (evenToNeg Q' Q h').comp (evenToNeg Q Q' h) = \\mathrm{AlgHom.id}_R$$$

Lean4

@[simp]
theorem evenToNeg_ι (Q' : QuadraticForm R M) (h : Q' = -Q) (m₁ m₂ : M) :
    evenToNeg Q Q' h ((even.ι Q).bilin m₁ m₂) = -(even.ι Q').bilin m₁ m₂ :=
  even.lift_ι _ _ m₁ m₂

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