Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-28 23:54 94800295

View on Github →

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

Estimated changes

Modified src/data/int/cast.lean

added theorem int.cast_add_hom_int

added theorem int.cast_ring_hom_int

Modified src/data/nat/cast.lean

added theorem nat.cast_ring_hom_nat

added theorem ring_hom.eq_nat_cast'

Modified src/data/rat/cast.lean

added theorem rat.cast_hom_rat