codRestrict — Mathlib

English

There is a scalar multiplication on ContinuousMultilinearMap by a ring R', compatible with toMultilinearMap and multilinear structure.

Русский

Существуют скалярные умножения на CMMap над кольцом R', совместимые с toMultilinearMap и мультиляйн структурой.

LaTeX

$$$\\text{SMul } R' (\\mathrm{ContinuousMultilinearMap} R M_1 M_2)$$$

Lean4

/-- Restrict the codomain of a continuous multilinear map to a submodule. -/
@[simps! toMultilinearMap apply_coe]
def codRestrict (f : ContinuousMultilinearMap R M₁ M₂) (p : Submodule R M₂) (h : ∀ v, f v ∈ p) :
    ContinuousMultilinearMap R M₁ p :=
  ⟨f.1.codRestrict p h, f.cont.subtype_mk _⟩

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