toNonUnitalSubalgebra_toSubmodule

English

The nonunital subalgebra obtained from a submodule via hmul, when reinterpreted as a submodule, recovers the original submodule.

Русский

Неполная подалгебра, полученная из подмодуля через hmul, если рассмотреть как подмодуль, восстанавливает исходный подмодуль.

LaTeX

$$$(p.toNonUnitalSubalgebra hmul).toSubmodule = p$$$

Lean4

@[simp]
theorem toNonUnitalSubalgebra_toSubmodule (p : Submodule R A) (h_mul) :
    (p.toNonUnitalSubalgebra h_mul).toSubmodule = p :=
  SetLike.coe_injective rfl

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