of_isotypicComponent_eq_top — Mathlib

English

If the isotypic component equals the top submodule, then the module is isotypic of the given type.

Русский

Если изотипическая компонента равна верхнему подподмодуля, тогда модуль является изотипическим по заданному типу.

LaTeX

$$$$ \\mathrm{isotypicComponent}(R,M,S) = \\top \\Rightarrow \\mathrm{IsIsotypicOfType}(R,M,S). $$$$

Lean4

theorem of_isotypicComponent_eq_top (h : isotypicComponent R M S = ⊤) : IsIsotypicOfType R M S := fun m _ ↦
  have ⟨_, ⟨e⟩, ⟨e'⟩⟩ := m.linearEquiv_of_sSup_eq_top _ h;
  ⟨e'.trans e⟩

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