Mathlib v3 is deprecated. Go to Mathlib v4

Theorem int.cast_ring_hom_int

Modification history

2022-03-28 23:54

src/data/int/cast.lean

chore(data/{nat,int,rat}/cast): add bundled version of `cast_id` lemmas (#13001)

Added int.cast_ring_hom_int View on Github →