dualProdDualEquivDual_apply — Mathlib

English

The canonical isomorphism sends a pair (φ, ψ) to the coproduct of φ and ψ in the dual of a product: dualProdDualEquivDual (φ, ψ) = φ.coprod ψ.

Русский

Стандартное отображение отправляет пары дуалов в дуальный функционал над произведением, соответствующий копродуту дуалов.

LaTeX

$$$\\text{dualProdDualEquivDual}\\, (\\phi,\\psi) = \\phi \\coprod \\psi$$$

Lean4

@[simp]
theorem dualProdDualEquivDual_apply (φ : Module.Dual R M) (ψ : Module.Dual R M') :
    dualProdDualEquivDual R M M' (φ, ψ) = φ.coprod ψ :=
  rfl

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