Commit 2026-09-09 22:48 01c8d16a

View on Github →

feat(Algebra/Module): use IsApply for LieHom (#42132) No obstacles in this one.

Estimated changes

deleted theorem LieEquiv.one_apply
deleted theorem LieHom.coe_one
deleted theorem LieHom.coe_zero
deleted theorem LieHom.one_apply
deleted theorem LieHom.zero_apply
deleted theorem LieModuleEquiv.one_apply
deleted theorem LieModuleHom.add_apply
deleted theorem LieModuleHom.coe_add
deleted theorem LieModuleHom.coe_neg
deleted theorem LieModuleHom.coe_nsmul
deleted theorem LieModuleHom.coe_smul
deleted theorem LieModuleHom.coe_sub
deleted theorem LieModuleHom.coe_zero
deleted theorem LieModuleHom.coe_zsmul
deleted theorem LieModuleHom.neg_apply
deleted theorem LieModuleHom.nsmul_apply
deleted theorem LieModuleHom.smul_apply
deleted theorem LieModuleHom.sub_apply
deleted theorem LieModuleHom.zero_apply
deleted theorem LieModuleHom.zsmul_apply