Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-25 16:55 44787193

View on Github →

feat(data/padic/padic_integers): homs to zmod(p ^ n) (#3882) This is the next PR in a series of PRs on the padic numbers/integers that should culminate in a proof that Z_p is isomorphic to the ring of Witt vectors of zmod p. In this PR we build ring homs from Z_p to zmod (p ^ n).

Estimated changes

added theorem int.to_nat_zero_of_neg
added theorem padic_int.appr_lt
added theorem padic_int.appr_spec
added theorem padic_int.coe_coe_int
added theorem padic_int.coe_int_eq
added theorem padic_int.ker_to_zmod
added theorem padic_int.to_zmod_spec
deleted theorem padic_norm.le_of_dvd
added theorem zmod.coe_to_nat