Theorem LinearEquiv.coe_prodUnique

Modification history

2025-06-19 13:45
Mathlib/LinearAlgebra/Prod.lean
feat: ContinuousLinearEquiv.{prodUnique,uniqueProd} (#26083) …
Added LinearEquiv.coe_prodUniqueView on Github →