Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-09-17 11:27
bfaffcf1
View on Github →
chore: bump to v4.1.0-rc1 (2nd attempt) (
#7216
)
Estimated changes
Modified
.github/workflows/bors.yml
Modified
.github/workflows/build.yml
Modified
.github/workflows/build.yml.in
Modified
.github/workflows/build_fork.yml
Modified
.gitignore
Modified
Archive/Imo/Imo1959Q1.lean
modified
theorem
imo1959_q1
Modified
Archive/Wiedijk100Theorems/PerfectNumbers.lean
Modified
GNUmakefile
Modified
Mathlib/Algebra/IsPrimePow.lean
modified
theorem
Nat.disjoint_divisors_filter_isPrimePow
Modified
Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
Modified
Mathlib/Data/Int/GCD.lean
modified
theorem
Nat.exists_mul_emod_eq_one_of_coprime
Modified
Mathlib/Data/Int/ModEq.lean
modified
theorem
Int.modEq_and_modEq_iff_modEq_mul
modified
theorem
Int.mod_coprime
Modified
Mathlib/Data/Nat/Choose/Central.lean
Modified
Mathlib/Data/Nat/Factorization/Basic.lean
modified
theorem
Nat.coprime_ord_compl
modified
theorem
Nat.factorization_disjoint_of_coprime
modified
theorem
Nat.factorization_eq_of_coprime_left
modified
theorem
Nat.factorization_eq_of_coprime_right
modified
theorem
Nat.factorization_mul_apply_of_coprime
modified
theorem
Nat.factorization_mul_of_coprime
modified
theorem
Nat.factorization_mul_support_of_coprime
Modified
Mathlib/Data/Nat/Factorization/PrimePow.lean
added
theorem
Nat.Coprime.isPrimePow_dvd_mul
deleted
theorem
Nat.coprime.isPrimePow_dvd_mul
modified
theorem
Nat.mul_divisors_filter_prime_pow
Modified
Mathlib/Data/Nat/Factors.lean
modified
theorem
Nat.coprime_factors_disjoint
modified
theorem
Nat.mem_factors_mul_of_coprime
modified
theorem
Nat.perm_factors_mul_of_coprime
Modified
Mathlib/Data/Nat/Fib.lean
modified
theorem
Nat.fib_coprime_fib_succ
Modified
Mathlib/Data/Nat/GCD/Basic.lean
added
theorem
Nat.Coprime.dvd_mul_left
added
theorem
Nat.Coprime.dvd_mul_right
added
theorem
Nat.Coprime.eq_of_mul_eq_zero
added
theorem
Nat.Coprime.lcm_eq_mul
added
theorem
Nat.Coprime.mul_add_mul_ne_mul
added
theorem
Nat.Coprime.symmetric
deleted
theorem
Nat.coprime.dvd_mul_left
deleted
theorem
Nat.coprime.dvd_mul_right
deleted
theorem
Nat.coprime.eq_of_mul_eq_zero
deleted
theorem
Nat.coprime.lcm_eq_mul
deleted
theorem
Nat.coprime.mul_add_mul_ne_mul
deleted
theorem
Nat.coprime.symmetric
modified
theorem
Nat.coprime_add_mul_left_left
modified
theorem
Nat.coprime_add_mul_left_right
modified
theorem
Nat.coprime_add_mul_right_left
modified
theorem
Nat.coprime_add_mul_right_right
modified
theorem
Nat.coprime_add_self_left
modified
theorem
Nat.coprime_add_self_right
modified
theorem
Nat.coprime_mul_left_add_left
modified
theorem
Nat.coprime_mul_left_add_right
modified
theorem
Nat.coprime_mul_right_add_left
modified
theorem
Nat.coprime_mul_right_add_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.gcd_mul_of_coprime_of_dvd
modified
theorem
Nat.not_coprime_zero_zero
Modified
Mathlib/Data/Nat/GCD/BigOperators.lean
Modified
Mathlib/Data/Nat/ModEq.lean
modified
def
Nat.chineseRemainder
modified
theorem
Nat.chineseRemainder_lt_mul
modified
theorem
Nat.coprime_of_mul_modEq_one
modified
theorem
Nat.modEq_and_modEq_iff_modEq_mul
Modified
Mathlib/Data/Nat/Periodic.lean
modified
theorem
Nat.periodic_coprime
Modified
Mathlib/Data/Nat/Prime.lean
modified
theorem
Nat.Prime.coprime_iff_not_dvd
modified
theorem
Nat.Prime.coprime_pow_of_not_dvd
modified
theorem
Nat.Prime.dvd_iff_not_coprime
modified
theorem
Nat.Prime.not_coprime_iff_dvd
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
Mathlib/Data/Nat/PrimeFin.lean
modified
theorem
Nat.factors_mul_toFinset_of_coprime
Modified
Mathlib/Data/Nat/Squarefree.lean
modified
theorem
Nat.coprime_of_squarefree_mul
modified
theorem
Nat.squarefree_mul
Modified
Mathlib/Data/Nat/Totient.lean
modified
theorem
Nat.totient_eq_card_coprime
modified
theorem
Nat.totient_eq_card_lt_and_coprime
modified
theorem
Nat.totient_mul
Modified
Mathlib/Data/PNat/Prime.lean
modified
theorem
PNat.Coprime.pow
modified
theorem
PNat.coprime_coe
Modified
Mathlib/Data/Rat/Defs.lean
Modified
Mathlib/Data/Rat/Denumerable.lean
Modified
Mathlib/Data/Rat/Encodable.lean
Modified
Mathlib/Data/Rat/Floor.lean
modified
theorem
Nat.coprime_sub_mul_floor_rat_div_of_coprime
Modified
Mathlib/Data/Rat/Lemmas.lean
modified
theorem
Rat.den_div_eq_of_coprime
modified
theorem
Rat.div_int_inj
modified
theorem
Rat.num_div_eq_of_coprime
Modified
Mathlib/Data/ZMod/Basic.lean
modified
def
ZMod.chineseRemainder
modified
theorem
ZMod.coe_mul_inv_eq_one
modified
theorem
ZMod.coe_unitOfCoprime
modified
def
ZMod.unitOfCoprime
modified
def
ZMod.unitsEquivCoprime
modified
theorem
ZMod.val_coe_unit_coprime
Modified
Mathlib/Dynamics/PeriodicPts.lean
Modified
Mathlib/FieldTheory/Finite/Basic.lean
modified
theorem
Nat.ModEq.pow_totient
Modified
Mathlib/GroupTheory/Complement.lean
Modified
Mathlib/GroupTheory/Exponent.lean
Modified
Mathlib/GroupTheory/NoncommPiCoprod.lean
Modified
Mathlib/GroupTheory/OrderOfElement.lean
modified
theorem
Commute.orderOf_mul_eq_mul_orderOf_of_coprime
modified
theorem
exists_pow_eq_self_of_coprime
modified
theorem
orderOf_pow_coprime
modified
theorem
powCoprime_inv
modified
theorem
powCoprime_one
Modified
Mathlib/GroupTheory/PGroup.lean
modified
theorem
IsPGroup.orderOf_coprime
modified
theorem
IsPGroup.powEquiv_apply
modified
theorem
IsPGroup.powEquiv_symm_apply
Modified
Mathlib/GroupTheory/Perm/Cycle/Basic.lean
modified
theorem
Equiv.Perm.closure_cycle_coprime_swap
Modified
Mathlib/GroupTheory/Perm/Sign.lean
modified
theorem
Equiv.Perm.support_pow_coprime
Modified
Mathlib/GroupTheory/SchurZassenhaus.lean
modified
theorem
Subgroup.eq_one_of_smul_eq_one
modified
theorem
Subgroup.exists_smul_eq
Modified
Mathlib/GroupTheory/Sylow.lean
Modified
Mathlib/Init/Data/Nat/GCD.lean
Modified
Mathlib/Lean/CoreM.lean
modified
def
CoreM.withImportModules
Modified
Mathlib/NumberTheory/ArithmeticFunction.lean
Modified
Mathlib/NumberTheory/FermatPsp.lean
modified
theorem
Nat.coprime_of_fermatPsp
Modified
Mathlib/NumberTheory/FrobeniusNumber.lean
modified
theorem
frobeniusNumber_pair
Modified
Mathlib/NumberTheory/NumberField/Units.lean
modified
theorem
NumberField.Units.rootsOfUnity_eq_one
Modified
Mathlib/NumberTheory/Padics/PadicVal.lean
Modified
Mathlib/NumberTheory/Padics/RingHoms.lean
Modified
Mathlib/NumberTheory/PellMatiyasevic.lean
modified
theorem
Pell.xy_coprime
Modified
Mathlib/NumberTheory/PrimeCounting.lean
Modified
Mathlib/NumberTheory/SumTwoSquares.lean
modified
theorem
ZMod.isSquare_neg_one_mul
Modified
Mathlib/NumberTheory/WellApproximable.lean
modified
theorem
approxOrderOf.image_pow_subset_of_coprime
modified
theorem
approxOrderOf.smul_subset_of_coprime
Modified
Mathlib/RingTheory/Coprime/Lemmas.lean
modified
theorem
Nat.isCoprime_iff_coprime
Modified
Mathlib/RingTheory/Int/Basic.lean
modified
theorem
Int.coprime_iff_nat_coprime
Modified
Mathlib/RingTheory/Multiplicity.lean
Modified
Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
Modified
Mathlib/RingTheory/RootsOfUnity/Basic.lean
modified
theorem
IsPrimitiveRoot.pow_of_coprime
Modified
Mathlib/RingTheory/RootsOfUnity/Complex.lean
modified
theorem
Complex.isPrimitiveRoot_exp_of_coprime
Modified
Mathlib/RingTheory/RootsOfUnity/Minpoly.lean
modified
theorem
IsPrimitiveRoot.minpoly_eq_pow_coprime
modified
theorem
IsPrimitiveRoot.pow_isRoot_minpoly
Modified
Mathlib/Tactic/NthRewrite.lean
deleted
def
Mathlib.Tactic.rewriteLocalDecl'
deleted
def
Mathlib.Tactic.rewriteTarget'
Modified
lake-manifest.json
Modified
lakefile.lean
Modified
lean-toolchain
Modified
scripts/checkYaml.lean
Renamed
scripts/runLinter.lean
to
scripts/runMathlibLinter.lean
Modified
test/norm_num_ext.lean
modified
theorem
ex11
modified
theorem
ex12
modified
theorem
ex13
modified
theorem
ex14
modified
theorem
ex15
modified
theorem
ex16'
modified
theorem
ex16
modified
theorem
ex17