associated_sq — Mathlib

English

For linear forms f,g: M→R, the associated quadratic form of linMulLin f g has polarization given by the symmetric combination 1/2(f(x)g(y)+f(y)g(x)).

Русский

Для линейных форм f,g: M→R квадратичная карта linMulLin f g имеет поляризацию, равную симметричному сочетанию 1/2(f(x)g(y)+f(y)g(x)).

LaTeX

$$$\\mathrm{associated}(\\mathrm{linMulLin}(f,g))(x,y) = \\tfrac{1}{2}\\bigl(f(x)g(y) + f(y)g(x)\\bigr).$$$

Lean4

@[simp]
theorem associated_sq [Invertible (2 : R)] : associated (R := R) sq = mul R R :=
  (associated_linMulLin (id) (id)).trans <| by simp only [smul_add, invOf_two_smul_add_invOf_two_smul]; rfl

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