Commit 2023-07-31 15:32 cebb5925

refactor(Algebra/Module/LinearMap): generalize the endomorphism algebra instance (#6207) Note that the module instance was already generalized; we were just missing the fact that when combined with the existing ring instance, the result was an algebra. This also moves some lemmas about IsUnit (_ : Module.End R M) to an earlier file as they are nothing to do with Algebra.