Commit 2023-02-13 18:55 28b8c15e
View on Github →fix: Add back LinearEquiv.coe_mk (#2253) This lemma was incorrectly deleted in #1732, after a mis-port caused it to be rejected as a tautology.
fix: Add back LinearEquiv.coe_mk (#2253) This lemma was incorrectly deleted in #1732, after a mis-port caused it to be rejected as a tautology.