of_isSimpleModule — Mathlib

English

Let M be a simple module over R. Then M is isotypic to itself: IsIsotypicOfType R M M.

Русский

Пусть M — простой модуль над R. Тогда M изотипичен к самому себе: IsIsotypicOfType R M M.

LaTeX

$$$IsIsotypicOfType(R, M, M)$$$

Lean4

theorem of_isSimpleModule [IsSimpleModule R M] : IsIsotypicOfType R M M := fun S hS ↦
  by
  rw [isSimpleModule_iff_isAtom, isAtom_iff_eq_top] at hS
  exact ⟨.trans (.ofEq _ _ hS) Submodule.topEquiv⟩

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