Theorem CharP.intCast_mul_natCast_gcdA_eq_gcd

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.intCast_mul_natCast_gcdA_eq_gcdView on Github →