Commit 2023-01-10 21:27 771dfd48

View on Github →

Revert "feat: port Mathlib.Data.Real.CauSeqCompletion (#1440)" (#1468) This reverts commit 0a713e2f48eb0380645a59f937d887edbf67f290. The motivation is to allow leanprover-community/mathlib#18122 to generate pre-port mathport output in the mathlib3port CI. Once that is done, I will unrevert this and merge in the changes it suggests.

Estimated changes

deleted theorem CauSeq.Completion.inv_mk
deleted theorem CauSeq.Completion.mk_add
deleted theorem CauSeq.Completion.mk_eq
deleted theorem CauSeq.Completion.mk_mul
deleted theorem CauSeq.Completion.mk_neg
deleted theorem CauSeq.Completion.mk_pow
deleted theorem CauSeq.Completion.mk_smul
deleted theorem CauSeq.Completion.mk_sub
deleted theorem CauSeq.complete
deleted theorem CauSeq.equiv_lim
deleted theorem CauSeq.le_lim
deleted theorem CauSeq.lim_add
deleted theorem CauSeq.lim_const
deleted theorem CauSeq.lim_eq_zero_iff
deleted theorem CauSeq.lim_inv
deleted theorem CauSeq.lim_le
deleted theorem CauSeq.lim_lt
deleted theorem CauSeq.lim_mul
deleted theorem CauSeq.lim_mul_lim
deleted theorem CauSeq.lim_neg
deleted theorem CauSeq.lt_lim