Commit 2025-03-11 14:15 2b937e66
View on Github →feat: numerals not divisible by the characteristic are invertible in rings (#22669)
We previously only had this for fields
Zulip thread, which suggests follow-up work to show the reverse implication (and an Iff).