English
Schur's Lemma implies that the endomorphism ring End_R(M) of a simple module M is a division ring.
Русский
Лемма Шура: кольцо эндоморфизмов End_R(M) простой модуля M является дивизионным кольцом.
LaTeX
$$DivisionRing(End_R(M)) [IsSimpleModule R M].$$
Lean4
/-- Schur's Lemma makes the endomorphism ring of a simple module a division ring. -/
noncomputable instance _root_.Module.End.instDivisionRing [DecidableEq (Module.End R M)] [IsSimpleModule R M] :
DivisionRing (Module.End R M)
where
inv f := if h : f = 0 then 0 else (LinearEquiv.ofBijective _ <| bijective_of_ne_zero h).symm
exists_pair_ne :=
⟨0, 1,
have := IsSimpleModule.nontrivial R M;
zero_ne_one⟩
mul_inv_cancel a
a0 := by
simp_rw [dif_neg a0]; ext
exact (LinearEquiv.ofBijective _ <| bijective_of_ne_zero a0).right_inv _
inv_zero := dif_pos rfl
nnqsmul := _
nnqsmul_def := fun _ _ => rfl
qsmul := _
qsmul_def := fun _ _ => rfl
