Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-01 20:53 dbb3ff0b

View on Github →

feat(data/zmod/quadratic_reciprocity): quadratic reciprocity (#327)

  • multiplicative group of finite field is cyclic
  • more stuff
  • change chinese remainder to def
  • get rid of nonsense
  • delete extra line break
  • one prod_bij left
  • move lemmas to correct places
  • delete prod_instances
  • almost done
  • move lamms to correct places
  • more moving lemmas
  • finished off moving lemmas
  • fix build
  • move quadratic reciprocity to zmod
  • improve readability
  • remove unnecessary alphas
  • move prod_range_id
  • fix build
  • fix build
  • fix build
  • fix build
  • delete mk_of_ne_zero
  • move odd_mul_odd_div_two
  • extra a few lemmas
  • improving readability
  • delete duplicate lemmas
  • forgot to save
  • delete duplicate lemma
  • indent calc proofs
  • fix build
  • fix build
  • forgot to save
  • fix build

Estimated changes

added theorem finset.card_bind
added theorem finset.card_bind_le
modified theorem finset.prod_const
modified theorem finset.prod_image
added theorem finset.prod_involution
added theorem finset.prod_nat_pow
added theorem finset.prod_pow
modified theorem finset.sum_const
added theorem finset.sum_smul
added theorem units.units.mk0_inj
added theorem units.coe_inv
added theorem units.coe_mul
added theorem units.coe_one
deleted theorem units.inv_coe
deleted theorem units.mul_coe
deleted theorem units.one_coe
added theorem units.coe_pow
added theorem one_lt_mul
added theorem finset.prod_mk_prod
added theorem units.coe_ne_zero
added theorem units.inv_eq_self_iff
modified theorem finset.card_attach
added theorem finset.card_congr
modified theorem finset.card_range
added theorem finset.card_union_le
modified theorem finset.fold_image
added theorem int.mod_mul_left_mod
added theorem int.mod_mul_right_mod
added theorem int.modeq.gcd_a_modeq
added theorem int.modeq.mod_modeq
added theorem nat.div_dvd_of_dvd
added theorem nat.pred_eq_sub_one
added theorem nat.succ_le_iff
added theorem nat.mod_mul_left_mod
added theorem nat.mod_mul_right_mod
added theorem nat.odd_mul_odd
added theorem nat.sum_totient
added def nat.totient
added theorem nat.totient_le
added theorem nat.totient_pos
modified theorem quotient.mk_out'
added theorem set.card_le_of_subset
added theorem zmod.coe_val_cast_int
added theorem zmod.ne_neg_self
added theorem zmodp.card_zmodp
added theorem zmodp.coe_val_cast_int
deleted theorem zmodp.gcd_a_modeq
added theorem zmodp.ne_neg_self
added theorem zmodp.prime_ne_zero
added theorem zmodp.card_units_zmodp
added theorem zmodp.euler_criterion
added theorem zmodp.fermat_little
added theorem zmodp.wilsons_lemma
added theorem order_of_pow
added theorem pow_card_eq_one
added theorem powers_eq_gpowers