Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_equiv.coe_to_int_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) …
Added add_equiv.coe_to_int_linear_equivView on Github →