restrict — Mathlib

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

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