ofEven_ι — Mathlib

English

For x,y ∈ M×R, the bilinear form through the even lift coincides with the product in the enlarged algebra after applying ι.

Русский

Для x,y ∈ M×R билинейная форма через приподнятие до четной части совпадает с произведением в расширенной алгебре после применения ι.

LaTeX

$$$(even.ι(Q').bilin x) \cdot (even.ι(Q').bilin y) = ι(Q' Q)(x) \cdot ι(Q' Q)(y)$$$

Lean4

theorem ofEven_ι (x y : M × R) :
    ofEven Q ((even.ι (Q' Q)).bilin x y) = (ι Q x.1 + algebraMap R _ x.2) * (ι Q y.1 - algebraMap R _ y.2) :=
  even.lift_ι (Q' Q) _ x y

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