top_lie_le_iff_le_normalizer — Mathlib

English

For any LieSubmodules N,N' of M, ⟦⊤, N⟧ ≤ N' iff N ≤ N'.normalizer.

Русский

Для любых подмодулов Ли N,N' подмодуль M: ⟦⊤, N⟧ ≤ N' тогда и только тогда, когда N ≤ N'.normalizer.

LaTeX

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

Lean4

theorem top_lie_le_iff_le_normalizer (N' : LieSubmodule R L M) : ⁅(⊤ : LieIdeal R L), N⁆ ≤ N' ↔ N ≤ N'.normalizer := by
  rw [lie_le_iff]; tauto

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