restrict — Mathlib

English

If B is symmetric on M, its restriction to any submodule W is symmetric.

Русский

Если B симметрична на M, то ограничение B на подмодуль W симметрично.

LaTeX

$$B.IsSymm → ∀ W : Submodule R M, (B.restrict W).IsSymm$$

Lean4

/-- The restriction of a symmetric bilinear form on a submodule is also symmetric. -/
theorem restrict {B : BilinForm R M} (b : B.IsSymm) (W : Submodule R M) : (B.restrict W).IsSymm :=
  ⟨fun x y => b.eq x y⟩

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