Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-12 10:19 30e620ce

View on Github →

chore(data/real/cau_seq): linting (#3040)

Estimated changes

modified theorem cau_seq.cauchy₂
modified theorem cau_seq.cauchy₃
modified theorem cau_seq.equiv_def₃
modified def cau_seq.inv
modified def cau_seq.lim_zero
modified theorem is_cau_seq.cauchy₂
modified theorem is_cau_seq.cauchy₃