toSubmodule_toNonUnitalSubalgebra

English

The round-trip in the opposite direction holds: starting from S, taking toSubmodule then toNonUnitalSubalgebra returns S.

Русский

Обратное прохождение: начиная с S, переход к Submodule, затем к NonUnitalSubalgebra возвращает S.

LaTeX

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

Lean4

@[simp]
theorem _root_.NonUnitalSubalgebra.toSubmodule_toNonUnitalSubalgebra (S : NonUnitalSubalgebra R A) :
    (S.toSubmodule.toNonUnitalSubalgebra fun _ _ => mul_mem (s := S)) = S :=
  SetLike.coe_injective rfl

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