Commit 2022-07-26 12:57 671d57dc
View on Github →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
-- TODO: define nat_cast/int_cast so that coe_coe and coe_coe_int are rfl