normalizer_inf — Mathlib

English

For LieSubmodules N,N' of M, the bracket with the whole Lie algebra satisfies ⟦⊤, N⟧ ≤ N' iff N ≤ N'.normalizer.

Русский

Для подмодулов Ли N и N' выполняется: ⟦⊤, N⟧ ≤ N' тогда и только тогда, когда N ≤ N'.normalizer.

LaTeX

$$$ [L,N] \\le N' \\iff N \\le N'.normalizer $$$

Lean4

theorem normalizer_inf : (N₁ ⊓ N₂).normalizer = N₁.normalizer ⊓ N₂.normalizer := by ext; simp [← forall_and]

Похожие утверждения