Mathlib v3 is deprecated. Go to Mathlib v4

Theorem cau_seq.is_cau

Modification history

2018-01-26 02:52

data/real/cau_seq.lean

feat(algebra/archimedean): generalize real thms to archimedean fields

Added cau_seq.is_cau View on Github →