Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-08 15:41 0c18d968

View on Github →

chore(data/padics/*): linting + squeeze_simp speedup (#4531)

Estimated changes

modified def padic_seq