Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-05 08:59 8898f0e2

View on Github →

feat(data/real/irrational): add basic irrational facts (#453) Joint work by Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Kenny Lau, and Chris Hughes

Estimated changes

added theorem int.nat_abs_pow
added theorem int.exists_mul_self
added def int.sqrt
added theorem int.sqrt_eq
added theorem int.sqrt_nonneg
added theorem nat.exists_mul_self
added theorem rat.abs_def
added theorem rat.cast_pow
added theorem rat.exists_mul_self
added theorem rat.mk_pnat_denom
added theorem rat.mk_pnat_num
added theorem rat.mul_denom
added theorem rat.mul_num
added theorem rat.mul_self_denom
added theorem rat.mul_self_num
added def rat.sqrt
added theorem rat.sqrt_eq
added theorem rat.sqrt_nonneg
added theorem irr_add_rat_iff_irr
added theorem irr_mul_rat_iff_irr
added theorem irr_neg
added theorem irr_nrt_of_notint_nrt
added theorem irr_of_irr_mul_self
added theorem irr_rat_add_iff_irr
added theorem irr_rat_add_of_irr
added theorem irr_sqrt_of_prime
added theorem irr_sqrt_rat_iff
added theorem irr_sqrt_two
deleted theorem sqrt_two_irrational