Commit 2023-12-17 21:55 27b7e3e7

View on Github →

feat: add CharP.natCast_eq_natCast_mod and relax typeclass assumptions (#9050)

Estimated changes

Modified Mathlib/Algebra/CharP/Basic.lean

added theorem CharP.intCast_eq_intCast_mod

added theorem CharP.natCast_eq_natCast'

modified theorem CharP.natCast_eq_natCast

added theorem CharP.natCast_eq_natCast_mod