Theorem invOf_eq_of_coprime

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