Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-04-08 18:50 284fdd29

View on Github →

chore(linear_algebra/alternating,topology/algebra/module/multilinear): add a fun_like instance (#18766)

Estimated changes

Modified src/analysis/analytic/inverse.lean

Modified src/analysis/calculus/cont_diff_def.lean

Modified src/analysis/normed_space/multilinear.lean

Modified src/linear_algebra/alternating.lean

Modified src/topology/algebra/module/multilinear.lean

deleted theorem continuous_multilinear_map.to_multilinear_map_inj

added theorem continuous_multilinear_map.to_multilinear_map_injective