Def LinearEquiv.uniqueProd

Modification history

2025-06-19 13:45
Mathlib/LinearAlgebra/Prod.lean
feat: ContinuousLinearEquiv.{prodUnique,uniqueProd} (#26083) …
Modified LinearEquiv.uniqueProdView on Github →
2025-05-06 11:37
Mathlib/LinearAlgebra/Prod.lean
feat: add {Alg,Linear}Equiv.{prodUnique,uniqueProd} (#24168) …
Added LinearEquiv.uniqueProdView on Github →