Theorem IsSimpleModule.congr

Modification history

2025-08-13 09:52

Mathlib/RingTheory/SimpleModule/Basic.lean

chore(RingTheory): use `extend` instead of `abbrev` in `IsS(emis)impleModule` (#27427)

Modified IsSimpleModule.congr View on Github →

2025-05-15 14:58

Mathlib/RingTheory/SimpleModule/Basic.lean

feat(RingTheory): isotypic API and simple Wedderburn–Artin existence (#23963) …

Modified IsSimpleModule.congr View on Github →

2023-04-06 14:19

Mathlib/RingTheory/SimpleModule.lean

feat: port RingTheory.SimpleModule (#3267)

Added IsSimpleModule.congr View on Github →