toSubmodule_le_toSubmodule — Mathlib

English

Let K and K' be Lie subalgebras of L over a commutative ring R. Then K ≤ K' as Lie subalgebras if and only if K ≤ K' when viewed as submodules of L; i.e., the order on Lie subalgebras coincides with the order induced by their underlying submodules.

Русский

Пусть K и K' — подалгебры Ли (K, K' ⊆ L) над кольцом R. Тогда K \le K' как подалгебры Ли тогда и только тогда, когда K \le K' как подмодули L; порядок над подалгебрами совпадает с порядком над их базовыми подмодулями.

LaTeX

$$$ (K : Submodule\\, R\\, L) \\le (K' : Submodule\\, R\\, L) \\iff K \\le K' $$$

Lean4

@[simp]
theorem toSubmodule_le_toSubmodule : (K : Submodule R L) ≤ K' ↔ K ≤ K' :=
  Iff.rfl

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