Commit 2025-09-06 10:02 aca523f7

View on Github →

feat: instances for ZeroHom and OneHom (#27305) This is motivated by wanting to write some lemmas about how the def in #27272 behaves on addition and scalar multiplcation, which requires these operations to first be defined. This shows that ZeroHom forms an AddCommGroup and Module, as well as analogous intermediate statements and OneHom results.

Estimated changes

added theorem OneHom.coe_div
added theorem OneHom.coe_inv
added theorem OneHom.coe_mul
added theorem OneHom.div_apply
added theorem OneHom.div_comp
added theorem OneHom.inv_apply
added theorem OneHom.inv_comp
added theorem OneHom.mul_apply
added theorem OneHom.mul_comp
added theorem OneHom.pow_apply
added theorem OneHom.zpow_apply
added theorem ZeroHom.coe_smul
added theorem ZeroHom.smul_apply
added theorem ZeroHom.smul_comp