English
If B is a bilinear form on M and W is a submodule of M, then the restriction of B to W defines a bilinear form on W, given by (B|_W)(u,v) = B(u,v) for u,v ∈ W.
Русский
Если B — билинейная форма на M, и W — подмодуль M, то ограничение B на W задаёт билинейную форму на W: (B|_W)(u,v) = B(u,v) для u,v ∈ W.
LaTeX
$$$$ (B|_W)(u,v)=B(u,v) \quad\text{for } u,v\in W. $$$$
Lean4
/-- The restriction of a bilinear form on a submodule. -/
@[simps! apply]
def restrict (B : BilinForm R M) (W : Submodule R M) : BilinForm R W :=
LinearMap.domRestrict₁₂ B W W