Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-21 23:57 5a652123

View on Github →

feat(data/real): real square root function, sqrt 2 is irrational

Estimated changes

Created algebra/char_zero.lean

added theorem add_group.char_zero_of_inj_zero

added theorem add_halves'

added theorem add_self_eq_zero

added theorem bit0_eq_zero

added theorem char_zero_of_inj_zero

added theorem half_add_self

added theorem half_sub

added theorem nat.cast_eq_zero

added theorem nat.cast_inj

added theorem nat.cast_injective

added theorem nat.cast_ne_zero

added theorem ordered_cancel_comm_monoid.char_zero_of_inj_zero

added theorem sub_half

added theorem two_ne_zero'

Modified algebra/field.lean

added theorem div_eq_iff_mul_eq

Modified algebra/group_power.lean

added theorem pow_two

added theorem smul_two

Modified algebra/ordered_field.lean

added theorem div_nonneg'

added theorem inv_lt_zero

added theorem inv_neg'

added theorem inv_nonneg

added theorem inv_nonpos

added theorem inv_pos'

added theorem mul_self_inj_of_nonneg

Modified algebra/ring.lean

added theorem bit0_eq_two_mul

Modified data/complex.lean

added theorem complex.add_conj

added theorem complex.eq_conj_iff_real

added theorem complex.of_real_bit0

added theorem complex.of_real_bit1

added theorem complex.of_real_div

added theorem complex.re_eq_add_conj

added theorem complex.sub_conj

Modified data/int/basic.lean

Modified data/nat/cast.lean

deleted theorem add_group.char_zero_of_inj_zero

deleted theorem char_zero_of_inj_zero

deleted theorem nat.cast_eq_zero

deleted theorem nat.cast_inj

deleted theorem nat.cast_injective

deleted theorem nat.cast_ne_zero

deleted theorem ordered_cancel_comm_monoid.char_zero_of_inj_zero

Modified data/nat/prime.lean

deleted theorem nat.dvd_of_prime_of_dvd_pow

added theorem nat.prime.dvd_of_dvd_pow

Modified data/real.lean

modified theorem cau_seq.cauchy₂

modified theorem cau_seq.cauchy₃

deleted def cau_seq.mk_of_near

deleted theorem cau_seq.mk_of_near_equiv

deleted theorem cau_seq.mk_of_near_fun

added theorem cau_seq.of_near

modified def cau_seq

added theorem is_cau_seq.cauchy₂

added theorem is_cau_seq.cauchy₃

added def is_cau_seq

added def real.irrational

added theorem real.is_cau_seq_iff_lift

added theorem real.mk_near_of_forall_near

added theorem real.mul_self_sqrt

added theorem real.of_near

added theorem real.sqr_sqrt

added def real.sqrt_aux

added theorem real.sqrt_aux_nonneg

added theorem real.sqrt_div

added theorem real.sqrt_eq_iff_mul_self_eq

added theorem real.sqrt_eq_iff_sqr_eq

added theorem real.sqrt_eq_zero'

added theorem real.sqrt_eq_zero

added theorem real.sqrt_eq_zero_of_nonpos

added theorem real.sqrt_exists

added theorem real.sqrt_inj

added theorem real.sqrt_inv

added theorem real.sqrt_le

added theorem real.sqrt_lt

added theorem real.sqrt_mul'

added theorem real.sqrt_mul

added theorem real.sqrt_mul_self

added theorem real.sqrt_nonneg

added theorem real.sqrt_one

added theorem real.sqrt_pos

added theorem real.sqrt_prop

added theorem real.sqrt_sqr

added theorem real.sqrt_two_irrational

added theorem real.sqrt_zero