mathlib

c5181d11 - feat(*): more `prod`-related (continuous) linear maps and their derivatives (#2277)

feat(*): more `prod`-related (continuous) linear maps and their derivatives (#2277) * feat(*): more `prod`-related (continuous) linear maps and their derivatives * Make `R` argument of `continuous_linear_equiv.refl` explicit Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>