Theorem Int.cast_injective

Modification history

2024-05-28 16:14

Mathlib/Data/Int/Cast/Lemmas.lean

chore: Do not import order theory in `Data.Int.Cast.Lemmas` (#13305) …

Modified Int.cast_injective View on Github →

2022-12-14 23:20

Mathlib/Data/Int/CharZero.lean

feat port: Data.Int.CharZero (#1029) …

Added Int.cast_injective View on Github →