Mathlib v3 is deprecated. Go to Mathlib v4

Theorem padic_int.coet_pow

Modification history

2020-12-16 15:31
src/data/padics/padic_integers.lean
chore(*): add a `div`/`sub` field to (`add_`)`group`(`_with_zero`) (#5303) …
Deleted padic_int.coet_powView on Github →
2020-10-05 08:49
src/data/padics/padic_integers.lean
feat(*): assorted `simp` lemmas for IMO 2019 q1 (#4383) …
Added padic_int.coet_powView on Github →