Commit 2023-09-15 12:48 6f8e8104

View on Github →

chore: bump to v4.1.0-rc1 (#7174) Some changes have already been review and delegated in #6910 and #7148. The diff that needs looking at is https://github.com/leanprover-community/mathlib4/pull/7174/commits/64d6d07ee18163627c8f517eb31455411921c5ac The std bump PR was insta-merged already!

Estimated changes

modified theorem imo1959_q1
modified theorem Int.mod_coprime
modified theorem Nat.coprime_ord_compl
modified theorem Nat.fib_coprime_fib_succ
added theorem Nat.Coprime.lcm_eq_mul
added theorem Nat.Coprime.symmetric
deleted theorem Nat.coprime.dvd_mul_left
deleted theorem Nat.coprime.dvd_mul_right
deleted theorem Nat.coprime.lcm_eq_mul
deleted theorem Nat.coprime.symmetric
modified theorem Nat.coprime_add_self_left
modified theorem Nat.coprime_add_self_right
modified theorem Nat.coprime_one_left_iff
modified theorem Nat.coprime_one_right_iff
modified theorem Nat.coprime_self_add_left
modified theorem Nat.coprime_self_add_right
modified theorem Nat.coprime_self_sub_left
modified theorem Nat.coprime_self_sub_right
modified theorem Nat.coprime_sub_self_left
modified theorem Nat.coprime_sub_self_right
modified theorem Nat.eq_one_of_dvd_coprimes
modified theorem Nat.not_coprime_zero_zero
modified def Nat.chineseRemainder
modified theorem Nat.chineseRemainder_lt_mul
modified theorem Nat.periodic_coprime
modified theorem Nat.coprime_of_dvd'
modified theorem Nat.coprime_of_dvd
modified theorem Nat.coprime_of_lt_prime
modified theorem Nat.coprime_or_dvd_of_prime
modified theorem Nat.coprime_primes
modified theorem Nat.prime_of_coprime
modified theorem Nat.squarefree_mul
modified theorem Nat.totient_eq_card_coprime
modified theorem Nat.totient_mul
modified theorem PNat.Coprime.pow
modified theorem PNat.coprime_coe
modified theorem Rat.den_div_eq_of_coprime
modified theorem Rat.div_int_inj
modified theorem Rat.num_div_eq_of_coprime
modified def ZMod.chineseRemainder
modified theorem ZMod.coe_mul_inv_eq_one
modified theorem ZMod.coe_unitOfCoprime
modified def ZMod.unitOfCoprime
modified theorem ZMod.val_coe_unit_coprime
modified theorem Nat.ModEq.pow_totient
modified theorem orderOf_pow_coprime
modified theorem powCoprime_inv
modified theorem powCoprime_one
modified theorem IsPGroup.orderOf_coprime
modified theorem IsPGroup.powEquiv_apply
modified theorem Subgroup.exists_smul_eq
modified theorem Nat.coprime_of_fermatPsp
modified theorem frobeniusNumber_pair
modified theorem Pell.xy_coprime
modified theorem ZMod.isSquare_neg_one_mul
modified theorem Nat.isCoprime_iff_coprime
modified theorem Int.coprime_iff_nat_coprime
modified theorem ex11
modified theorem ex12
modified theorem ex13
modified theorem ex14
modified theorem ex15
modified theorem ex16'
modified theorem ex16
modified theorem ex17