basis): remove unhelpful coercion (#10637)

Commit

4 years ago

chore(linear_algebra/affine_space/basis): remove unhelpful coercion (#10637) It is more useful to have a statement of equality of linear maps than of raw functions.

Author

ocfnash

Committer

jcommelin

Parents

8438172d

mathlib3 1ad1be71 - chore(linear_algebra/affine_space/basis): remove unhelpful coercion (#10637)

mathlib3
1ad1be71 - chore(linear_algebra/affine_space/basis): remove unhelpful coercion (#10637)