noncomputable def prodTopLinearEquiv {k : Type u_1} [Field k] {V₁ : Type u_2} [AddCommGroup V₁] [Module k V₁] {V₂ : Type u_3} [AddCommGroup V₂] [Module k V₂] (W₂ : Submodule k V₂) : ↥(⊤.prod W₂) ≃ₗ[k] V₁ × ↥W₂

Linear equivalence identifying the product submodule ⊤ × W₂ ⊆ V₁ × V₂ with the external product V₁ × W₂.