Def invertibleOfCoprime

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 invertibleOfCoprimeView on Github →