Theorem Odd.intCast

Modification history

2024-06-08 16:29

Mathlib/Data/Int/Cast/Lemmas.lean

chore: Move `CharP` lemmas about order of elements (#12816) …

Modified Odd.intCast View on Github →

2024-06-05 21:47

Mathlib/Data/Int/Cast/Lemmas.lean

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

Added Odd.intCast View on Github →