Theorems · Theorem · ring theory

Module.End.IsSemisimple.of_mem_adjoin_pair

∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_1 : Field K] [inst_2 : Module K M] {f g : Module.End K M}
  [FiniteDimensional K M] [PerfectField K],
  Commute f g → f.IsSemisimple → g.IsSemisimple → ∀ {a : Module.End K M}, a ∈ K[f, g] → a.IsSemisimple

Defined in

Mathlib.LinearAlgebra.Semisimple

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommGroupFieldModuleFiniteDimensionalPerfectField