Mathlib Map

Theorems · Theorem · ring theory

Module.End.IsSemisimple_smul_iff

∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_1 : Field K] [inst_2 : Module K M] {f : Module.End K M}
  {t : K}, t ≠ 0 → ((t • f).IsSemisimple ↔ f.IsSemisimple)
Defined in
Mathlib.LinearAlgebra.Semisimple
Cited by
1 results in Mathlib
Foundations
Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddCommGroupFieldModule
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Module.End.IsSemisimple_smul · cited by 0End.IsSemisimple_smulModule · cited by 20661ModuleRingHom.id · cited by 18349RingHom.idAddCommGroup · cited by 12871AddCommGroupField · cited by 7404FieldSubmodule · cited by 7192SubmoduleModule.End · cited by 774Module.EndIsCompl · cited by 351IsComplSubmodule.comap · cited by 347Submodule.comapModule.End.IsSemisimple · cited by 34End.IsSemisimpleSubmodule.comap_smul · cited by 4Submodule.comap_smulEnd.IsSemisimple_smul_iffCITED BYCITES

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.