English
The associated bilinear form of the squaring quadratic map equals the standard multiplication bilinear form.
Русский
Ассоциированная билинейная форма квадратичной карты квадратичного возведения равна обычной форме умножения.
LaTeX
$$$\\mathrm{associated}(\\mathrm{sq}) = \\mathrm{mul}_{R,R}$.$$
Lean4
@[simp]
theorem associated_linMulLin [Invertible (2 : R)] (f g : M →ₗ[R] R) :
associated (R := R) (N := R) (linMulLin f g) = ⅟(2 : R) • ((mul R R).compl₁₂ f g + (mul R R).compl₁₂ g f) :=
by
ext
simp only [associated_apply, linMulLin_apply, map_add, smul_add, LinearMap.add_apply, LinearMap.smul_apply,
compl₁₂_apply, mul_apply', smul_eq_mul, invOf_smul_eq_iff]
simp only [Module.End.smul_def, Module.End.ofNat_apply, nsmul_eq_mul, Nat.cast_ofNat, mul_invOf_cancel_left']
ring_nf
