of_subsingleton — Mathlib

English

In a subsingleton environment, IsIsotypic holds; all simple submodules are isomorphic to any fixed S.

Русский

В среде subsingleton IsIsotypic выполняется; все простые подподмодули изоморфны любому фиксированному S.

LaTeX

$$IsIsotypic R M := IsIsotypicOfType R M S.$$

Lean4

@[nontriviality]
theorem of_subsingleton [Subsingleton M] : IsIsotypic R M := fun S ↦
  (IsIsotypicOfType.of_subsingleton R M S).isIsotypic S

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