Commit 2023-05-27 16:11 082fcd0f

View on Github →

feat: port NumberTheory.Padics.RingHoms (#4395) A coercion in a previous file (done by me) was wrong so I fix it in this PR

Estimated changes

added theorem PadicInt.appr_lt
added theorem PadicInt.appr_mono
added theorem PadicInt.appr_spec
added theorem PadicInt.isUnit_den
added theorem PadicInt.ker_toZMod
added theorem PadicInt.ker_toZModPow
added def PadicInt.lift
added theorem PadicInt.lift_self
added theorem PadicInt.lift_spec
added theorem PadicInt.lift_unique
added theorem PadicInt.limNthHom_add
added theorem PadicInt.limNthHom_mul
added theorem PadicInt.limNthHom_one
added def PadicInt.modPart
added theorem PadicInt.modPart_lt_p
added def PadicInt.nthHom
added theorem PadicInt.nthHomSeq_add
added theorem PadicInt.nthHomSeq_mul
added theorem PadicInt.nthHomSeq_one
added theorem PadicInt.nthHom_zero
added def PadicInt.toZMod
added theorem PadicInt.toZMod_spec
added theorem PadicInt.zmodRepr_lt_p
added theorem PadicInt.zmodRepr_spec