mathlib

54c286db - feat(data/{nat,int,rat}/cast, algebra/star/basic): lemmas about `star` on casts (#12418)

feat(data/{nat,int,rat}/cast, algebra/star/basic): lemmas about `star` on casts (#12418) This also includes lemmas about `mul_opposite` on casts which are used to prove the star lemmas. The new lemmas are: * `star_nat_cast` * `star_int_cast` * `star_rat_cast` * `op_nat_cast` * `op_int_cast` * `op_rat_cast` * `unop_nat_cast` * `unop_int_cast` * `unop_rat_cast`