isotypicComponent — Mathlib

English

If a submodule m is in the isotypicComponents of M, then m is IsIsotypic.

Русский

Если подпмодуль m принадлежит множеству isotypicComponents(M), тогда m является IsIsotypic.

LaTeX

$$$$ m \\in \\mathrm{isotypicComponents}(R,M) \\Rightarrow \\mathrm{IsIsotypic}(R,m). $$$$

Lean4

protected theorem isotypicComponent : IsIsotypicOfType R (isotypicComponent R M S) S :=
  isIsotypicOfType_submodule_iff.mpr fun m h _ ↦
    have ⟨_, ⟨e⟩, ⟨e'⟩⟩ := m.linearEquiv_of_le_sSup _ h
    ⟨e'.trans e⟩

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