mathlib3
8e281044 - feat(algebra/algebra/basic): define `restrict_scalars.linear_equiv` (#7807)

Commit
4 years ago
feat(algebra/algebra/basic): define `restrict_scalars.linear_equiv` (#7807) Also updating some doc-strings.
Author
Parents
Loading