English
A module M is simple iff it is nontrivial and every nonzero x ∈ M generates M via SpanSingleton surjectivity.
Русский
Модуль M прост тогда и только тогда, когда он не тривиален и каждый ненулевой элемент генерирует M через сюръективность SpanSingleton.
LaTeX
$$IsSimpleModule R M ↔ (Nontrivial M ∧ ∀ x ∈ M, x ≠ 0 → Surjective (toSpanSingleton R M x))$$
Lean4
/-- 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. -/
theorem annihilator_isMaximal {R} [CommRing R] [Module R M] [simple : IsSimpleModule R M] :
(Module.annihilator R M).IsMaximal :=
by
have ⟨I, max, ⟨e⟩⟩ := isSimpleModule_iff_quot_maximal.mp simple
rwa [e.annihilator_eq, I.annihilator_quotient]
