Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_equiv.coe_to_linear_equiv

Modification history

2022-01-17 21:04
src/data/equiv/module.lean
feat(data/equiv/basic): add `add_equiv.to_int_linear_equiv` (#11456) …
Modified add_equiv.coe_to_linear_equivView on Github →
2020-10-05 11:38
src/linear_algebra/basic.lean
feat(data/finsupp): Make `finsupp.dom_congr` a `≃+` (#4398) …
Added add_equiv.coe_to_linear_equivView on Github →