toSubmodule_inj — Mathlib

English

Equality of the submodules induced by LieSubmodule corresponds to equality of the LieSubmodules themselves.

Русский

Равенство соответствующих подмодулей порождается равенством самих подмодулей Ли.

LaTeX

$$∀ {N N' : LieSubmodule R L M}, (N.toSubmodule = N'.toSubmodule) ↔ N = N'$$

Lean4

@[simp]
theorem toSubmodule_inj : (N : Submodule R M) = (N' : Submodule R M) ↔ N = N' :=
  toSubmodule_injective.eq_iff

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