Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-01 18:06 a8076b2c

View on Github →

refactor(data/real/irrational): review (#2304)

  • refactor(data/real/irrational): review
  • Update src/data/real/irrational.lean
  • Update src/data/real/irrational.lean
  • Apply suggestions from code review

Estimated changes

deleted theorem irr_add_rat_iff_irr
deleted theorem irr_mul_rat_iff_irr
deleted theorem irr_neg
deleted theorem irr_nrt_of_notint_nrt
deleted theorem irr_of_irr_mul_self
deleted theorem irr_rat_add_iff_irr
deleted theorem irr_rat_add_of_irr
deleted theorem irr_sqrt_of_prime
deleted theorem irr_sqrt_rat_iff
deleted theorem irr_sqrt_two
added theorem irrational.add_cases
added theorem irrational.add_rat
added theorem irrational.div_cases
added theorem irrational.mul_cases
added theorem irrational.mul_rat
added theorem irrational.of_add_rat
added theorem irrational.of_fpow
added theorem irrational.of_inv
added theorem irrational.of_mul_rat
added theorem irrational.of_mul_self
added theorem irrational.of_neg
added theorem irrational.of_one_div
added theorem irrational.of_pow
added theorem irrational.of_rat_add
added theorem irrational.of_rat_div
added theorem irrational.of_rat_mul
added theorem irrational.of_rat_sub
added theorem irrational.of_sub_rat
added theorem irrational.rat_add
added theorem irrational.rat_mul
added theorem irrational.rat_sub
added theorem irrational.sub_rat
modified def irrational
added theorem irrational_add_rat_iff
added theorem irrational_inv_iff
added theorem irrational_neg_iff
added theorem irrational_rat_add_iff
added theorem irrational_rat_sub_iff
added theorem irrational_sqrt_two
added theorem irrational_sub_rat_iff
added theorem rat.not_irrational