Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-05 08:57 94b09d65

View on Github →

refactor(data/real/basic): make real irreducible (#454)

Estimated changes

Modified analysis/complex.lean

Modified analysis/limits.lean

modified theorem tendsto_pow_at_top_at_top_of_gt_1_nat

Modified analysis/real.lean

Modified data/complex/basic.lean

modified theorem complex.I_mul_I

modified theorem complex.conj_I

modified theorem complex.conj_neg_I

modified theorem complex.conj_of_real

modified theorem complex.conj_one

modified theorem complex.conj_zero

modified theorem complex.norm_sq_I

modified theorem complex.norm_sq_one

modified theorem complex.norm_sq_zero

modified theorem complex.of_real_add

modified theorem complex.of_real_bit0

modified theorem complex.of_real_bit1

modified theorem complex.of_real_neg

modified theorem complex.of_real_sub

Modified data/complex/exponential.lean

Modified data/padics/hensel.lean

Modified data/real/basic.lean

added def real.comm_ring_aux

added def real.mk

added theorem real.mk_eq

added theorem real.mk_eq_mk

added theorem real.quotient_mk_eq_mk