Theorem LinearEquiv.coe_prodCongr

Modification history

2025-04-19 15:05

Mathlib/LinearAlgebra/Prod.lean

chore: rename LinearEquiv.prod to prodCongr (#24145) …

Added LinearEquiv.coe_prodCongr View on Github →