Commit 2023-05-22 21:00 20f9f921

View on Github →

feat: port Data.Real.Irrational (#4234)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Real/Irrational.lean

added theorem Int.not_irrational

added theorem Irrational.add_cases

added theorem Irrational.add_int

added theorem Irrational.add_nat

added theorem Irrational.add_rat

added theorem Irrational.div_cases

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_cases

added theorem Irrational.mul_int

added theorem Irrational.mul_nat

added theorem Irrational.mul_rat

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_add_rat

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_inv

added theorem Irrational.of_mul_int

added theorem Irrational.of_mul_nat

added theorem Irrational.of_mul_rat

added theorem Irrational.of_mul_self

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_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_int

added theorem Irrational.of_sub_nat

added theorem Irrational.of_sub_rat

added theorem Irrational.of_zpow

added theorem Irrational.rat_add

added theorem Irrational.rat_div

added theorem Irrational.rat_mul

added theorem Irrational.rat_sub

added theorem Irrational.sub_int

added theorem Irrational.sub_nat

added theorem Irrational.sub_rat

added def Irrational

added theorem Nat.Prime.irrational_sqrt

added theorem Nat.not_irrational

added theorem Rat.not_irrational

added theorem Transcendental.irrational

added theorem exists_irrational_btwn

added theorem irrational_add_int_iff

added theorem irrational_add_nat_iff

added theorem irrational_add_rat_iff

added theorem irrational_div_int_iff

added theorem irrational_div_nat_iff

added theorem irrational_div_rat_iff

added theorem irrational_iff_ne_rational

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_inv_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_neg_iff

added theorem irrational_nrt_of_n_not_dvd_multiplicity

added theorem irrational_nrt_of_notint_nrt

added theorem irrational_rat_add_iff

added theorem irrational_rat_div_iff

added theorem irrational_rat_mul_iff

added theorem irrational_rat_sub_iff

added theorem irrational_sqrt_of_multiplicity_odd

added theorem irrational_sqrt_rat_iff

added theorem irrational_sqrt_two

added theorem irrational_sub_int_iff

added theorem irrational_sub_nat_iff

added theorem irrational_sub_rat_iff

added theorem one_lt_natDegree_of_irrational_root