Theorem LinearEquiv.coe_uniqueProd

Modification history

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