multilinear): add a fun_like instance (#18766)

Commit

2 years ago

chore(linear_algebra/alternating,topology/algebra/module/multilinear): add a fun_like instance (#18766) Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

Author

eric-wieser

Parents

36172d66

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

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