mathlib
dd114987 - chore(linear_algebra/basic): redefine `restrict` (#5229)

Commit

5 years ago

chore(linear_algebra/basic): redefine `restrict` (#5229) Use `dom_restrict` and `cod_restrict`

Author

urkud

Parents