mathlib
8ac2fa06 - chore(linear_algebra/affine_space/affine_map): make `affine_map.coe_sub` true by definition (#10182)

Commit
4 years ago
chore(linear_algebra/affine_space/affine_map): make `affine_map.coe_sub` true by definition (#10182) This makes life slightly easier in some work following on from https://github.com/leanprover-community/mathlib/pull/10161 Formalized as part of the Sphere Eversion project.
Author
Parents
Loading