Commit 2021-05-05 13:56 1823aeef

View on Github →

feat(algebra/module): S-linear equivs are also R-linear equivs (#7476) This PR extends linear_map.restrict_scalars to linear_equivs. To be used in the bundled-basis refactor.

Estimated changes

Modified src/algebra/module/linear_map.lean

added def linear_equiv.restrict_scalars