instNontrivialSubtypeMemSubmoduleValSetIsotypicComponents

English

The set isotypicComponents R M consists of submodules of M isomorphic to some simple submodule S.

Русский

Множество isotypicComponents R M состоит из подпмодулей M, изоморфных некоторому простому подпмодулю S.

LaTeX

$$$\text{isotypicComponents}(R, M) = \{ m : \text{Submodule}_R(M) \mid \exists S, IsSimpleModule(R, S) \land m = isotypicComponent(R, M, S) \}$$$

Lean4

instance (c : isotypicComponents R M) : Nontrivial c :=
  Submodule.nontrivial_iff_ne_bot.mpr (bot_lt_isotypicComponents c.2).ne'

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