Theorems · Theorem · ring theory

Module.End.isSemisimple_restrict_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}
  (p : Submodule R M) (hp : p ∈ f.invtSubmodule),
  Module.End.IsSemisimple (LinearMap.restrict f hp) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p

Defined in

Mathlib.LinearAlgebra.Semisimple

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule