Theorems · Theorem · ring theory

Module.End.isFinitelySemisimple_iff

∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {f : Module.End R M},
  f.IsFinitelySemisimple ↔
    ∀ p ∈ f.invtSubmodule,
      Module.Finite R ↥p → ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p

A characterisation of Module.End.IsFinitelySemisimple using only the lattice of submodules of M (thus avoiding submodules of submodules).

Defined in

Mathlib.LinearAlgebra.Semisimple

Cited by

2 results in Mathlib

Foundations

Depth 130 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModule