Commit 2023-02-01 19:20 938fead7

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.