mathlib3

671d57dc - chore(number_theory/padics/padic_integers): golf the comm_ring instance (#15590)

chore(number_theory/padics/padic_integers): golf the comm_ring instance (#15590) This results in nicer definitional equalities that don't involve the application of a recursor. This also renames `padic_int.coe_coe` to `padic_int.coe_nat_cast` and `padic_int.coe_coe_int` to `padic_int.coe_int_cast` to match other similar lemmas in mathlib. Finally, this fixes the TODO comment ```lean -- TODO: define nat_cast/int_cast so that coe_coe and coe_coe_int are rfl ```