Commit 2023-01-06 13:41 f35d518e

View on Github →

chore: rename some 'int_cast' to 'intCast' (#1337)

Estimated changes

added theorem MulOpposite.op_intCast
deleted theorem MulOpposite.op_int_cast
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