dualProdDualEquivDual — Mathlib

English

Taking duals distributes over products: the dual of a product of two modules is canonically isomorphic to the product of their duals.

Русский

Дуальность распадается по произведению: дуал пространство произведения равно каноническому произведению дуалов отдельных пространств.

LaTeX

$$$ (Module.Dual\\, R\\, M \\times Module.Dual\\, R\\, M') \\cong_{R} Module.Dual\\, R\\, (M \\times M') $$$

Lean4

/-- Taking duals distributes over products. -/
@[simps!]
def dualProdDualEquivDual : (Module.Dual R M × Module.Dual R M') ≃ₗ[R] Module.Dual R (M × M') :=
  LinearMap.coprodEquiv R

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