Commit 2021-05-27 09:01 5360e476

View on Github →

feat(algebra/module/linear_map): linear_(map|equiv).restrict_scalars is injective (#7725) So as not to repeat them for the lemmas, I moved the typeclasses into a variables statement.

Estimated changes

Modified src/algebra/module/linear_map.lean

modified def linear_equiv.restrict_scalars

added theorem linear_equiv.restrict_scalars_inj

added theorem linear_equiv.restrict_scalars_injective

modified def linear_map.restrict_scalars

added theorem linear_map.restrict_scalars_inj

added theorem linear_map.restrict_scalars_injective