Mathlib Changelog
v4
Changelog
About
Github
Theorem
IsArtinianRing.isNilpotent_nilradical
Modification history
2025-02-04 14:13
Mathlib/RingTheory/Artinian/Ring.lean
feat(RingTheory): unramified iff `κ(q)/κ(p)` is separable and `pS_q = qS_q` (#20690)
Added
IsArtinianRing.isNilpotent_nilradical
View on Github →