Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes

modified theorem padic_int.coe_add
deleted theorem padic_int.coe_coe
deleted theorem padic_int.coe_coe_int
added theorem padic_int.coe_int_cast
modified theorem padic_int.coe_mul
added theorem padic_int.coe_nat_cast
modified theorem padic_int.coe_neg
modified theorem padic_int.coe_pow
modified theorem padic_int.coe_sub
modified theorem padic_int.ext
modified theorem padic_int.mk_coe
modified theorem padic_int.nonarchimedean
modified theorem padic_int.norm_le_one
modified theorem padic_int.norm_p
modified theorem padic_int.norm_p_pow