Commit 2024-06-05 21:47 464cfc74

View on Github →

feat: add {Even,Odd}.natCast (#13405)

Estimated changes

Modified Mathlib/Algebra/Ring/Parity.lean

added theorem Odd.natCast

Modified Mathlib/Data/Int/Cast/Lemmas.lean

added theorem Int.Even.intCast

added theorem Odd.intCast

Modified Mathlib/Data/Nat/Cast/Basic.lean

added theorem Even.natCast