Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-01-06 13:41
f35d518e
View on Github →
chore: rename some 'int_cast' to 'intCast' (
#1337
)
Estimated changes
Modified
Mathlib/Data/Int/Cast/Lemmas.lean
added
theorem
AddMonoidHom.eq_int_castAddHom
deleted
theorem
AddMonoidHom.eq_int_cast_hom
added
theorem
MulOpposite.op_intCast
deleted
theorem
MulOpposite.op_int_cast
added
theorem
MulOpposite.unop_intCast
deleted
theorem
MulOpposite.unop_int_cast
added
theorem
RingHom.eq_intCast'
deleted
theorem
RingHom.eq_int_cast'
added
theorem
eq_intCast'
added
theorem
eq_intCast
deleted
theorem
eq_int_cast'
deleted
theorem
eq_int_cast
added
theorem
map_intCast
deleted
theorem
map_int_cast
added
theorem
ofDual_intCast
deleted
theorem
ofDual_int_cast
added
theorem
ofLex_intCast
deleted
theorem
ofLex_int_cast
added
theorem
toDual_intCast
deleted
theorem
toDual_int_cast
added
theorem
toLex_intCast
deleted
theorem
toLex_int_cast
Modified
Mathlib/Data/Rat/Cast.lean