instIsSimpleModuleSubtypeMemSubmoduleValSetSetOfNonemptyLinearEquivId

English

If there is a linear isomorphism between a submodule m of M and a simple module S (with IsSimpleModule R S), then m is itself a simple R-module.

Русский

Если существует линейное изоморфизм между подмодулем m подмодуля M и простым модулем S, то сам m является простым R-модулем.

LaTeX

$$$$ \\exists e: m \\cong_R S \\;\\Rightarrow\\; m \\text{ is simple}. $$$$

Lean4

local instance (m : {m : Submodule R M | Nonempty (m ≃ₗ[R] S)}) : IsSimpleModule R m :=
  .congr m.2.some

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