Mathlib Changelog
v3
Changelog
About
Github
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
src/data/real/cau_seq.lean
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₃