Theorem CharP.isUnit_natCast_iff

Modification history

2025-03-11 14:15
Mathlib/Algebra/CharP/Invertible.lean
feat: numerals not divisible by the characteristic are invertible in rings (#22669) …
Added CharP.isUnit_natCast_iffView on Github →