Theorem RingCon.nontrivial_iff

Modification history

2025-05-01 06:42
Mathlib/RingTheory/Congruence/Basic.lean
feat: preliminaries for Wedderburn–Artin (#24119)
Added RingCon.nontrivial_iffView on Github →