Commit 2025-06-19 13:45 4516ade2

View on Github →

feat: ContinuousLinearEquiv.{prodUnique,uniqueProd} (#26083) which are LinearEquiv.{prodUnique,uniqueProd} as a continuous linear equivalence. Discovered when working on slice models for defining submanifolds (#24550), one step towards defining smooth submanifolds. This PR continues the work from #23971.

Estimated changes

Modified Mathlib/LinearAlgebra/Prod.lean

added theorem LinearEquiv.coe_prodUnique

added theorem LinearEquiv.coe_uniqueProd

modified def LinearEquiv.prodUnique

modified def LinearEquiv.uniqueProd

Modified Mathlib/Topology/Algebra/Module/Equiv.lean

added theorem ContinuousLinearEquiv.coe_prodUnique

added theorem ContinuousLinearEquiv.coe_uniqueProd

added def ContinuousLinearEquiv.prodUnique

added theorem ContinuousLinearEquiv.prodUnique_apply

added theorem ContinuousLinearEquiv.prodUnique_symm_apply

added def ContinuousLinearEquiv.uniqueProd

added theorem ContinuousLinearEquiv.uniqueProd_apply

added theorem ContinuousLinearEquiv.uniqueProd_symm_apply