isFinitelySemisimple_iff_isSemisimple

English

Under Module.Finite, IsFinitelySemisimple is equivalent to IsSemisimple (variant variant).

Русский

При Module.Finite IsFinitelySemisimple эквивалентно IsSemisimple.

LaTeX

$$$ [Module.Finite R M] \Rightarrow (IsFinitelySemisimple(f) \iff IsSemisimple(f))$$$

Lean4

@[simp]
theorem isFinitelySemisimple_iff_isSemisimple [Module.Finite R M] : f.IsFinitelySemisimple ↔ f.IsSemisimple :=
  by
  refine ⟨fun hf ↦ isSemisimple_iff.mpr fun p hp ↦ ?_, IsSemisimple.isFinitelySemisimple⟩
  obtain ⟨q, -, hq₁, hq₂, hq₃⟩ := isFinitelySemisimple_iff.mp hf ⊤ (invtSubmodule.top_mem f) inferInstance p hp le_top
  exact ⟨q, hq₁, hq₂, codisjoint_iff.mpr hq₃⟩

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