Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-06-12 22:37 99101eac

View on Github →

feat(data/num/basic): add div,mod,gcd for num,znum

Estimated changes

Modified algebra/ordered_ring.lean

added theorem mul_lt_mul''

Modified data/int/basic.lean

added theorem int.coe_nat_div

added theorem int.mem_to_nat'

modified theorem int.neg_succ_of_nat_div

modified theorem int.of_nat_div

added def int.to_nat'

Modified data/num/basic.lean

added def num.div2

added def num.div

added def num.gcd

added def num.gcd_aux

added def num.mod

added def num.nat_size

added def pos_num.div'

added def pos_num.divmod

added def pos_num.divmod_aux

added def pos_num.mod'

added def pos_num.nat_size

added def pos_num.sqrt_aux1

added def pos_num.sqrt_aux

added def znum.abs

added def znum.div

added def znum.gcd

added def znum.mod

Modified data/num/lemmas.lean

added theorem num.cast_bit0

added theorem num.cast_bit1

added theorem num.cast_of_znum

added theorem num.cast_pos

added theorem num.div_to_nat

added theorem num.dvd_iff_mod_eq_zero

added theorem num.dvd_to_nat

added theorem num.gcd_to_nat

added theorem num.gcd_to_nat_aux

added theorem num.mem_of_znum'

added theorem num.mod_to_nat

added theorem num.nat_size_to_nat

modified theorem num.of_nat_to_znum

modified theorem num.of_nat_to_znum_neg

added theorem num.of_znum'_to_nat

added theorem num.of_znum_to_nat

added theorem num.size_eq_nat_size

added theorem num.size_to_nat

added theorem num.sub_to_nat

added theorem num.to_nat_to_int

modified theorem pos_num.cast_inj

added theorem pos_num.div'_to_nat

added theorem pos_num.divmod_to_nat

added theorem pos_num.divmod_to_nat_aux

added theorem pos_num.mod'_to_nat

added theorem pos_num.nat_size_pos

added theorem pos_num.nat_size_to_nat

added theorem pos_num.size_eq_nat_size

added theorem pos_num.to_int_eq_succ_pred

added theorem pos_num.to_nat_eq_succ_pred

added theorem pos_num.to_nat_to_int

added theorem znum.abs_to_nat

added theorem znum.div_to_int

added theorem znum.dvd_iff_mod_eq_zero

added theorem znum.dvd_to_int

added theorem znum.gcd_to_nat

added theorem znum.mod_to_int