mathlib

c0cc689b - chore(algebra/lie/direct_sum): remove `direct_sum.lie_algebra_is_internal` (#15631)

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: ```lean 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.