isotypicComponent_eq_top_iff — Mathlib

English

Under mild assumptions, the S-isotypic component equals top iff the module is isotypic of type S.

Русский

При определённых условиях S-изотипическая компонента равна топу тогда, когда модуль изотипичен по типу S.

LaTeX

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

Lean4

theorem isotypicComponent_eq_top_iff [IsSemisimpleModule R M] : isotypicComponent R M S = ⊤ ↔ IsIsotypicOfType R M S :=
  by rw [← top_le_iff, le_isotypicComponent_iff, Submodule.topEquiv.isIsotypicOfType_iff]

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