mulMap' — Mathlib

English

Another articulation that mulMap equals mul' composed with mapIncl.

Русский

Еще одно выражение того, что mulMap равен mul' композиции mapIncl.

LaTeX

$$$mulMap M N = mul' R S \circ TensorProduct.mapIncl M N$$$

Lean4

/-- If `M` and `N` are submodules in an algebra `S` over `R`, there is the natural `R`-linear map
`M ⊗[R] N →ₗ[R] M * N` induced by multiplication in `S`,
which is surjective (`Submodule.mulMap'_surjective`). -/
def mulMap' : M ⊗[R] N →ₗ[R] ↥(M * N) :=
  (LinearEquiv.ofEq _ _ (mulMap_range M N)).toLinearMap ∘ₗ (mulMap M N).rangeRestrict

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