Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-13 17:57 3faf0f5d

View on Github →

chore(data/real/irrational): add more lemmas (#9684)

Estimated changes

added theorem int.not_irrational
added theorem irrational.add_int
added theorem irrational.add_nat
added theorem irrational.div_int
added theorem irrational.div_nat
added theorem irrational.div_rat
added theorem irrational.int_add
added theorem irrational.int_div
added theorem irrational.int_mul
added theorem irrational.int_sub
added theorem irrational.mul_int
added theorem irrational.mul_nat
added theorem irrational.nat_add
added theorem irrational.nat_div
added theorem irrational.nat_mul
added theorem irrational.nat_sub
added theorem irrational.ne_int
added theorem irrational.ne_nat
added theorem irrational.ne_one
added theorem irrational.ne_rat
added theorem irrational.ne_zero
added theorem irrational.of_add_int
added theorem irrational.of_add_nat
added theorem irrational.of_div_int
added theorem irrational.of_div_nat
added theorem irrational.of_div_rat
added theorem irrational.of_int_add
added theorem irrational.of_int_div
added theorem irrational.of_int_mul
added theorem irrational.of_int_sub
added theorem irrational.of_mul_int
added theorem irrational.of_mul_nat
added theorem irrational.of_nat_add
added theorem irrational.of_nat_div
added theorem irrational.of_nat_mul
added theorem irrational.of_nat_sub
added theorem irrational.of_sub_int
added theorem irrational.of_sub_nat
added theorem irrational.rat_div
added theorem irrational.sub_int
added theorem irrational.sub_nat
added theorem irrational_add_int_iff
added theorem irrational_add_nat_iff
added theorem irrational_div_int_iff
added theorem irrational_div_nat_iff
added theorem irrational_div_rat_iff
added theorem irrational_int_add_iff
added theorem irrational_int_div_iff
added theorem irrational_int_mul_iff
added theorem irrational_int_sub_iff
added theorem irrational_mul_int_iff
added theorem irrational_mul_nat_iff
added theorem irrational_mul_rat_iff
added theorem irrational_nat_add_iff
added theorem irrational_nat_div_iff
added theorem irrational_nat_mul_iff
added theorem irrational_nat_sub_iff
added theorem irrational_rat_div_iff
added theorem irrational_rat_mul_iff
added theorem irrational_sub_int_iff
added theorem irrational_sub_nat_iff
added theorem nat.not_irrational
modified theorem rat.not_irrational