toSubmodule_injective — Mathlib

English

The map sending a subalgebra to its underlying submodule is injective: if two subalgebras have the same underlying submodule, then they are equal.

Русский

Отображение, отправляющее подалгебру в её базовый подмодуль, инъективно: если две подалгебры имеют одинаковый базовый подмодуль, то они равны.

LaTeX

$$$(\forall S_1,S_2)\; toSubmodule(S_1) = toSubmodule(S_2) \Rightarrow S_1 = S_2$$$

Lean4

theorem toSubmodule_injective : Function.Injective (toSubmodule : Subalgebra R A → Submodule R A) := fun _S₁ _S₂ h =>
  SetLike.ext (SetLike.ext_iff.mp h :)

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