Theorem isSimpleRing_iff_isTwoSided_imp

Modification history

2025-05-01 06:42
Mathlib/RingTheory/SimpleRing/Congr.lean
feat: preliminaries for Wedderburn–Artin (#24119)
Added isSimpleRing_iff_isTwoSided_impView on Github →