Commit 2024-05-04 21:00 83a590b7

View on Github →

feat: add NonUnital{Star}AlgHom.restrictScalars (#12657)

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalHom.lean

added theorem NonUnitalAlgHom.coe_restrictScalars'

added theorem NonUnitalAlgHom.coe_restrictScalars

added def NonUnitalAlgHom.restrictScalars

added theorem NonUnitalAlgHom.restrictScalars_apply

added theorem NonUnitalAlgHom.restrictScalars_injective

Modified Mathlib/Algebra/Star/StarAlgHom.lean

added theorem NonUnitalStarAlgHom.coe_restrictScalars'

added theorem NonUnitalStarAlgHom.coe_restrictScalars

added def NonUnitalStarAlgHom.restrictScalars

added theorem NonUnitalStarAlgHom.restrictScalars_apply

added theorem NonUnitalStarAlgHom.restrictScalars_injective