Theorem CharP.natCast_gcdA_mul_intCast_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.natCast_gcdA_mul_intCast_eq_gcdView on Github →