Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-21 05:51 f5987b2a

View on Github →

chore(data/real/basic): tweak lemmas about of_cauchy (#12829) These lemmas are about real.of_cauchy not real.cauchy, as their name suggests. This also flips the direction of some of the lemmas to be consistent with the zero and one lemmas. Finally, this adds the lemmas about real.cauchy that are missing.

Estimated changes

deleted theorem real.add_cauchy
added theorem real.cauchy_add
added theorem real.cauchy_inv
added theorem real.cauchy_mul
added theorem real.cauchy_neg
added theorem real.cauchy_one
added theorem real.cauchy_zero
deleted theorem real.inv_cauchy
modified theorem real.mk_add
modified theorem real.mk_mul
modified theorem real.mk_neg
modified theorem real.mk_one
modified theorem real.mk_zero
deleted theorem real.mul_cauchy
deleted theorem real.neg_cauchy
added theorem real.of_cauchy_add
added theorem real.of_cauchy_inv
added theorem real.of_cauchy_mul
added theorem real.of_cauchy_neg
added theorem real.of_cauchy_one
added theorem real.of_cauchy_zero
deleted theorem real.one_cauchy
deleted theorem real.zero_cauchy