English
Define a bilinear form on S over R by B(x,y) = Tr_{S/R}(xy). This bilinear form is symmetric, and it is nondegenerate if the extension is separable.
Русский
Задаем билинейную форму B(x,y) = Tr_{S/R}(xy) на S над R. Эта форма симметрична и непредобрачна (невырождается) если расширение сепарабельно.
LaTeX
$$$B(x,y) = \\operatorname{trace}_{S/R}(xy)$ and $B$ is symmetric; if the extension is separable then $B$ is nondegenerate.$$
Lean4
/-- The `traceForm` maps `x y : S` to the trace of `x * y`.
It is a symmetric bilinear form and is nondegenerate if the extension is separable. -/
@[stacks 0BIK "Trace pairing"]
noncomputable def traceForm : BilinForm R S :=
LinearMap.compr₂ (lmul R S).toLinearMap (trace R S)
