mathlib

938fead7 - fix(algebra/lie/*): use correct terminology for `centralizer` and `normalizer` in Lie theory (#18348)

fix(algebra/lie/*): use correct terminology for `centralizer` and `normalizer` in Lie theory (#18348) The naming here was wrong. If `N : lie_submodule R L M` then: * `{ m : M | ∀ (x : L), ⁅x, m⁆ ∈ N }` is the carrier of the _normalizer_ of `N`. If `N : set M` then: * `{ x : L | ∀ (m ∈ N), ⁅x, (m : M)⁆ = 0 }` is the carrier of the _centralizer_ of `N`. [No formal definition yet, seems important not to restrict `N` to be a `lie_submodule` since an important case is to apply this to `M = L` regarded as a Lie module over itself and `N` a `lie_subalgebra` of `L` (but not necessarily a `lie_ideal`). Note this generalises `lie_module.ker`.] I'm a bit shocked I got this muddled originally.