polar_prod — Mathlib

English

If x and y are pairs (x1,x2) and (y1,y2) in M1×M2, then the polar form of the product equals the sum of the polar forms on each component.

Русский

Если x=(x1,x2), y=(y1,y2) в M1×M2, то полярная форма произведения равна сумме полярных форм по компонентам.

LaTeX

$$$ \\mathrm{polar}((Q_1 \\text{ prod } Q_2))(x,y) = \\mathrm{polar}(Q_1)(x_1,y_1) + \\mathrm{polar}(Q_2)(x_2,y_2). $$$

Lean4

@[simp]
theorem polar_prod (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (x y : M₁ × M₂) :
    polar (Q₁.prod Q₂) x y = polar Q₁ x.1 y.1 + polar Q₂ x.2 y.2 :=
  by
  dsimp [polar]
  abel

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