Commit 2023-03-02 21:54 cc4cbb73

View on Github →

feat: port Algebra.Algebra.RestrictScalars (#2563)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Algebra/RestrictScalars.lean

added def RestrictScalars.addEquiv

added theorem RestrictScalars.addEquiv_map_smul

added theorem RestrictScalars.addEquiv_symm_map_algebraMap_smul

added theorem RestrictScalars.addEquiv_symm_map_smul_smul

added def RestrictScalars.lsmul

added theorem RestrictScalars.lsmul_apply_apply

added def RestrictScalars.moduleOrig

added def RestrictScalars.ringEquiv

added theorem RestrictScalars.ringEquiv_algebraMap

added theorem RestrictScalars.ringEquiv_map_smul

added def RestrictScalars

added theorem restrictScalars.smul_def