Mathlib v3 is deprecated. Go to Mathlib v4

Theorem simple_iff_is_simple_module'

Modification history

2022-12-04 12:16
src/algebra/category/Module/simple.lean
feat(algebra/category/Module/simple): 1d modules over k-algebras are simple (#14023) …
Added simple_iff_is_simple_module'View on Github →