Theorems · Theorem · ring theory

IsSimpleModule.annihilator_isMaximal

∀ {M : Type u_4} [inst : AddCommGroup M] {R : Type u_6} [inst_1 : CommRing R] [inst_2 : Module R M]
  [simple : IsSimpleModule R M], (Module.annihilator R M).IsMaximal

In general, the annihilator of a simple module is called a primitive ideal, and it is always a two-sided prime ideal, but mathlib's Ideal.IsPrime is not the correct definition for noncommutative rings.

Defined in

Mathlib.RingTheory.SimpleModule.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommGroupCommRingModuleIsSimpleModule