toSubmodule_le_toSubmodule — Mathlib

English

For LieSubmodules N,N', the order relation is preserved by underlying Submodules: (N : Submodule R M) ≤ N' if and only if N ≤ N'.

Русский

Для подмодулей Ли N,N' верно: (N как Submodule) ≤ N' тогда и только тогда, когда N ≤ N' как подмодули Ли.

LaTeX

$$$ (N : Submodule R M) \le N' \iff N \le N' $$$

Lean4

@[simp, norm_cast]
theorem toSubmodule_le_toSubmodule : (N : Submodule R M) ≤ N' ↔ N ≤ N' :=
  Iff.rfl

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