Commit 2025-10-14 10:42 89e22b1c
View on Github →refactor: add LinearMapClass and LinearEquivClass instances to Lie(Module)Hom and Equiv (#30450)
Adding these instances means we can use general linearity lemmas like map_add without needing a specialized version like LieHom.map_add. Because these specialized lemmata become superfluous, this PR deprecates them.