Commit 2024-04-18 10:42 838bc130

View on Github →

chore: Rename isnatCast, delete Int.cast_Nat_cast (#12236) Int.cast_Nat_cast dates back to the ad-hoc port, in #206.

Estimated changes

Modified Mathlib/Algebra/Ring/Int.lean

deleted theorem Int.cast_Nat_cast

Modified Mathlib/Tactic/NormNum/Basic.lean

added theorem Mathlib.Meta.NormNum.isNat_natCast

deleted theorem Mathlib.Meta.NormNum.isnatCast

Modified Mathlib/Tactic/ReduceModChar.lean