Commit 2022-07-23 14:34 c0cc689b

chore(algebra/lie/direct_sum): remove direct_sum.lie_algebra_is_internal (#15631) This meant the same thing as the unprefixed version, and wasn't used anywhere:

example [decidable_eq ι] : direct_sum.lie_algebra_is_internal I ↔ direct_sum.is_internal I := iff.rfl

I think it was added before direct_sum.is_internal generalized to arbitrary additive subobjects.