Commit 2024-04-25 01:30 1fd4ce47

View on Github →

feat(Algebra/GroupWithZero/WithZero): WithZero.map' (#12159)

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/WithZero.lean

added def WithZero.coeMonoidHom

added theorem WithZero.lift'_coe

added theorem WithZero.lift'_unique

added theorem WithZero.lift'_zero

added theorem WithZero.map'_coe

added theorem WithZero.map'_comp

added theorem WithZero.map'_id

added theorem WithZero.map'_map'

added theorem WithZero.map'_zero

added theorem WithZero.monoidWithZeroHom_ext

added theorem WithZero.unzero_mul