Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-06-10 08:38 004e0b30

View on Github →

feat (data/pnat): extensions to pnat (#1073)

  • Extended API, especially divisibility and primes
  • Positive euclidean algorithm
  • Disambiguate overloaded ::
  • Tweak broken proof of flip_is_special
  • Change to mathlib style
  • Update src/data/pnat.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • Update src/data/pnat.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • Adjust style for mathlib
  • Moved and renamed
  • Move some material from basic.lean to prime.lean
  • Move some material from basic.lean to factors.lean
  • Update import to data.pnat.basic.
  • Update import to data.pnat.basic
  • Fix import of data.pnat.basic
  • Use monoid.pow instead of nat.pow
  • Fix pnat.pow_succ -> pow_succ; stylistic changes
  • More systematic use of coercion
  • More consistent use of coercion
  • Formatting; change flip' to prod.swap

Estimated changes

added theorem nat.primes.coe_nat_inj
added def nat.primes
deleted def nat.succ_pnat
deleted theorem nat.succ_pnat_coe
deleted def nat.to_pnat'
deleted def nat.to_pnat
deleted theorem pnat.add_coe
deleted theorem pnat.coe_to_pnat'
deleted theorem pnat.eq
deleted theorem pnat.mk_coe
deleted theorem pnat.mul_coe
deleted theorem pnat.ne_zero
deleted theorem pnat.one_coe
deleted theorem pnat.pos
deleted def pnat.pow
deleted theorem pnat.pow_coe
deleted theorem pnat.to_pnat'_coe
deleted def pnat
added def nat.succ_pnat
added theorem nat.succ_pnat_coe
added theorem nat.succ_pnat_inj
added def nat.to_pnat'
added theorem nat.to_pnat'_coe
added def nat.to_pnat
added theorem pnat.add_coe
added theorem pnat.add_sub_of_lt
added theorem pnat.coe_to_pnat'
added def pnat.div
added theorem pnat.div_coe
added def pnat.div_exact
added theorem pnat.dvd_antisymm
added theorem pnat.dvd_gcd
added theorem pnat.dvd_iff''
added theorem pnat.dvd_iff'
added theorem pnat.dvd_iff
added theorem pnat.dvd_intro
added theorem pnat.dvd_lcm_left
added theorem pnat.dvd_lcm_right
added theorem pnat.dvd_one_iff
added theorem pnat.dvd_refl
added theorem pnat.dvd_trans
added theorem pnat.eq
added def pnat.gcd
added theorem pnat.gcd_coe
added theorem pnat.gcd_dvd_left
added theorem pnat.gcd_dvd_right
added theorem pnat.gcd_mul_lcm
added def pnat.lcm
added theorem pnat.lcm_coe
added theorem pnat.lcm_dvd
added theorem pnat.mk_coe
added def pnat.mod
added theorem pnat.mod_add_div
added theorem pnat.mod_coe
added def pnat.mod_div
added def pnat.mod_div_aux
added theorem pnat.mod_div_aux_spec
added theorem pnat.mod_le
added theorem pnat.mul_coe
added theorem pnat.mul_div_exact
added theorem pnat.ne_zero
added theorem pnat.one_coe
added theorem pnat.one_dvd
added theorem pnat.pos
added theorem pnat.pow_coe
added def pnat.prime
added theorem pnat.sub_coe
added theorem pnat.to_pnat'_coe
added def pnat
added def prime_multiset
added def pnat.gcd_a'
added theorem pnat.gcd_a'_coe
added theorem pnat.gcd_a_eq
added def pnat.gcd_b'
added theorem pnat.gcd_b'_coe
added theorem pnat.gcd_b_eq
added def pnat.gcd_d
added theorem pnat.gcd_det_eq
added theorem pnat.gcd_eq
added theorem pnat.gcd_props
added theorem pnat.gcd_rel_left'
added theorem pnat.gcd_rel_left
added theorem pnat.gcd_rel_right'
added theorem pnat.gcd_rel_right
added def pnat.gcd_w
added def pnat.gcd_x
added def pnat.gcd_y
added def pnat.gcd_z
added def pnat.xgcd:
added def pnat.xgcd_type.a
added def pnat.xgcd_type.b
added theorem pnat.xgcd_type.flip_a
added theorem pnat.xgcd_type.flip_b
added theorem pnat.xgcd_type.flip_v
added theorem pnat.xgcd_type.flip_w
added theorem pnat.xgcd_type.flip_x
added theorem pnat.xgcd_type.flip_y
added theorem pnat.xgcd_type.flip_z
added def pnat.xgcd_type.q
added theorem pnat.xgcd_type.qp_eq
added def pnat.xgcd_type.r
added theorem pnat.xgcd_type.rq_eq
added theorem pnat.xgcd_type.start_v
added theorem pnat.xgcd_type.step_v
added theorem pnat.xgcd_type.step_wf
added def pnat.xgcd_type.v
added def pnat.xgcd_type.w
added def pnat.xgcd_type.z
added structure pnat.xgcd_type