Commit 2021-11-05 15:19 8ac2fa06
View on Github →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.