IsIsotypicOfType — Mathlib

English

If an R-module M has a type-S isotypic condition on simple submodules, then M is isotypic.

Русский

Если M имеет изотипическое отношение по простым субмодулям типа S, то M изотипичен.

LaTeX

$$IsIsotypic (IsIsotypicOfType R M S) → IsIsotypic R M.$$

Lean4

/-- An `R`-module `M` is isotypic of type `S` if all simple submodules of `M` are isomorphic
to `S`. If `M` is semisimple, it is equivalent to requiring that all simple quotients of `M` are
isomorphic to `S`. -/
def IsIsotypicOfType : Prop :=
  ∀ (m : Submodule R M) [IsSimpleModule R m], Nonempty (m ≃ₗ[R] S)

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