dualDistrib — Mathlib

English

A heterobasic version of the dual distribution map provides a linear map from Dual_A M ⊗_R Dual_R N to Dual_A (M ⊗_R N).

Русский

Гетеробазисная версия отображения dualDistrib задаёт линейное отображение от Dual_A M ⊗_R Dual_R N к Dual_A (M ⊗_R N).

LaTeX

$$$$ dualDistrib : Dual_A M \\otimes_R Dual_R N \\to_{\\,A} Dual_A (M \\otimes_R N). $$$$

Lean4

/-- Heterobasic version of `TensorProduct.dualDistrib` -/
def dualDistrib : Dual A M ⊗[R] Dual R N →ₗ[A] Dual A (M ⊗[R] N) :=
  compRight _ (Algebra.TensorProduct.rid R A A).toLinearMap ∘ₗ homTensorHomMap R A A M N A R

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