mulMap — Mathlib

English

For m ∈ M and n ∈ N, mulMap M N (m ⊗ n) equals the product m.1 · n.1 in S.

Русский

Для m ∈ M и n ∈ N, mulMap M N на m ⊗ n равно произведению m.1 · n.1 в S.

LaTeX

$$$mulMap M N (m \otimes_R n) = m.1 \cdot n.1$$$

Lean4

/-- If `M` and `N` are submodules in an algebra `S` over `R`, there is the natural `R`-linear map
`M ⊗[R] N →ₗ[R] S` induced by multiplication in `S`. -/
def mulMap : M ⊗[R] N →ₗ[R] S :=
  TensorProduct.lift ((LinearMap.mul R S).domRestrict₁₂ M N)

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