mk — Mathlib · SciLib

English

There is a heterobasic version of TensorProduct.uncurry providing a linear map M ⊗R N →A P from a bilinear map M →A N →R P.

Русский

Существует гетеробазовая версия TensorProduct.uncurry, задающая линейное отображение M ⊗R N →A P из билинейного отображения M →A N →R P.

LaTeX

$$$\text{uncurry} : (M \to_A N \to_R P) \to_B M \otimes_R N \to_A P$$$

Lean4

/-- Heterobasic version of `TensorProduct.mk`:

The canonical bilinear map `M →[A] N →[R] M ⊗[R] N`. -/
@[simps! apply]
nonrec def mk (A M N : Type*) [Semiring A] [AddCommMonoid M] [Module R M] [Module A M] [SMulCommClass R A M]
    [AddCommMonoid N] [Module R N] : M →ₗ[A] N →ₗ[R] M ⊗[R] N :=
  { mk R M N with map_smul' := fun _ _ => rfl }

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