Commit 2023-06-24 03:33 ab70224a

View on Github →

feat: add Unitization.starLift (#5102) A NonUnitalStarAlgHom from A to C (over a ring R) lifts uniquely to a StarAlgHom from Unitization R A to C.

Estimated changes

Modified Mathlib/Algebra/Algebra/Unitization.lean

added theorem NonUnitalAlgHom.toAlgHom_zero

added theorem Unitization.algHom_ext''

modified theorem Unitization.algHom_ext

added theorem Unitization.algebraMap_eq_inlRingHom

deleted theorem Unitization.algebraMap_eq_inl_hom

added def Unitization.inrNonUnitalStarAlgHom

added theorem Unitization.starAlgHom_ext

added def Unitization.starLift

added theorem Unitization.starLift_symm_apply_apply

Modified Mathlib/Algebra/Star/StarAlgHom.lean

added theorem NonUnitalStarAlgHom.coe_mk'

added theorem StarAlgHom.coe_mk'