mathlib

292bf34d - feat(algebra/lie/ideal_operations): add lemma `lie_ideal_oper_eq_linear_span'` (#11823)

feat(algebra/lie/ideal_operations): add lemma `lie_ideal_oper_eq_linear_span'` (#11823) It is useful to have this alternate form in situations where we have a hypothesis like `h : I = J` since we can then rewrite using `h` after applying this lemma. An (admittedly brief) scan of the existing applications of `lie_ideal_oper_eq_linear_span` indicates that it's worth keeping both forms for convenience but I'm happy to dig deeper into this if requested.