Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-11 01:12 cf4c49c4

View on Github →

chore(data/real/cau_seq_completion): remove use of parameters (#18122) This helps with porting

Estimated changes

Modified src/data/real/basic.lean

modified def real.equiv_Cauchy

modified def real.ring_equiv_Cauchy

Modified src/data/real/cau_seq_completion.lean

modified theorem cau_seq.completion.inv_zero

modified def cau_seq.completion.mk

modified theorem cau_seq.completion.mk_eq

modified theorem cau_seq.completion.mk_eq_mk

modified theorem cau_seq.completion.mk_eq_zero

modified def cau_seq.completion.of_rat

modified theorem cau_seq.completion.of_rat_add

modified theorem cau_seq.completion.of_rat_div

modified theorem cau_seq.completion.of_rat_int_cast

modified theorem cau_seq.completion.of_rat_inv

modified theorem cau_seq.completion.of_rat_mul

modified theorem cau_seq.completion.of_rat_nat_cast

modified theorem cau_seq.completion.of_rat_neg

modified theorem cau_seq.completion.of_rat_one

modified theorem cau_seq.completion.of_rat_rat_cast

modified def cau_seq.completion.of_rat_ring_hom

modified theorem cau_seq.completion.of_rat_sub

modified theorem cau_seq.completion.of_rat_zero

modified theorem cau_seq.completion.zero_ne_one