Commit 2023-01-10 21:12 0a713e2f

View on Github →

feat: port Mathlib.Data.Real.CauSeqCompletion (#1440)

depends on: #1124 This is quite painful due to parameter use in mathlib3.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Real/CauSeqCompletion.lean

added def CauSeq.Completion.Cauchy

added theorem CauSeq.Completion.cau_seq_zero_ne_one

added theorem CauSeq.Completion.inv_mk

added theorem CauSeq.Completion.inv_zero

added def CauSeq.Completion.mk

added theorem CauSeq.Completion.mk_add

added theorem CauSeq.Completion.mk_eq

added theorem CauSeq.Completion.mk_eq_mk

added theorem CauSeq.Completion.mk_eq_zero

added theorem CauSeq.Completion.mk_mul

added theorem CauSeq.Completion.mk_neg

added theorem CauSeq.Completion.mk_pow

added theorem CauSeq.Completion.mk_smul

added theorem CauSeq.Completion.mk_sub

added def CauSeq.Completion.ofRat

added def CauSeq.Completion.ofRatRingHom

added theorem CauSeq.Completion.ofRat_add

added theorem CauSeq.Completion.ofRat_div

added theorem CauSeq.Completion.ofRat_intCast

added theorem CauSeq.Completion.ofRat_inv

added theorem CauSeq.Completion.ofRat_mul

added theorem CauSeq.Completion.ofRat_natCast

added theorem CauSeq.Completion.ofRat_neg

added theorem CauSeq.Completion.ofRat_one

added theorem CauSeq.Completion.ofRat_ratCast

added theorem CauSeq.Completion.ofRat_sub

added theorem CauSeq.Completion.ofRat_zero

added theorem CauSeq.Completion.zero_ne_one

added theorem CauSeq.complete

added theorem CauSeq.eq_lim_of_const_equiv

added theorem CauSeq.equiv_lim

added theorem CauSeq.le_lim

added theorem CauSeq.lim_add

added theorem CauSeq.lim_const

added theorem CauSeq.lim_eq_lim_of_equiv

added theorem CauSeq.lim_eq_of_equiv_const

added theorem CauSeq.lim_eq_zero_iff

added theorem CauSeq.lim_inv

added theorem CauSeq.lim_le

added theorem CauSeq.lim_lt

added theorem CauSeq.lim_mul

added theorem CauSeq.lim_mul_lim

added theorem CauSeq.lim_neg

added theorem CauSeq.lt_lim