Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-04 21:33 7734d386

View on Github →

refactor(data/real/basic): make ℝ a structure (#6024) Preparation for :four_leaf_clover:, which doesn't have irreducible.

Estimated changes

added theorem real.add_cauchy
deleted def real.comm_ring_aux
added theorem real.ext_cauchy
added theorem real.ext_cauchy_iff
added theorem real.inv_cauchy
added theorem real.lt_cauchy
modified def real.mk
added theorem real.mk_add
modified theorem real.mk_eq
deleted theorem real.mk_eq_mk
modified theorem real.mk_le_of_forall_le
modified theorem real.mk_lt
added theorem real.mk_mul
added theorem real.mk_neg
added theorem real.mk_one
added theorem real.mk_zero
added theorem real.mul_cauchy
added theorem real.neg_cauchy
modified def real.of_rat
added theorem real.of_rat_apply
modified theorem real.of_rat_lt
deleted theorem real.of_rat_sub
added theorem real.one_cauchy
deleted theorem real.quotient_mk_eq_mk
added theorem real.zero_cauchy
added structure real
deleted def real
added theorem equiv.cardinal_eq