Commit 2023-09-15 16:52 40b58304

View on Github →

Revert "chore: bump to v4.1.0-rc1 (#7174)" (#7198) This reverts commit 6f8e81040eae7655f51d145b8026569b91d66e0d. Unfortunately this bump was not linted correctly, as CI did not run runLinter Mathlib. We can unrevert once that's fixed.

Estimated changes

modified theorem imo1959_q1
modified theorem Int.mod_coprime
modified theorem Nat.coprime_ord_compl
modified theorem Nat.fib_coprime_fib_succ
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
added theorem Nat.coprime.lcm_eq_mul
added 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