Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-01-13 09:10
d4e2fbc7
View on Github →
feat: port Data.Real.CauSeqCompletion (
#1469
) Unreverts
#1440
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