Commit 2023-01-20 01:29 35976074

View on Github →

feat: port RingTheory.Coprime.Lemmas (#1692)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Logic/Basic.lean

added theorem exists_apply_eq

Created Mathlib/RingTheory/Coprime/Lemmas.lean

added theorem Finset.prod_dvd_of_coprime

added theorem Fintype.prod_dvd_of_coprime

added theorem IsCoprime.of_prod_left

added theorem IsCoprime.of_prod_right

added theorem IsCoprime.pow

added theorem IsCoprime.pow_iff

added theorem IsCoprime.pow_left

added theorem IsCoprime.pow_left_iff

added theorem IsCoprime.pow_right

added theorem IsCoprime.pow_right_iff

added theorem IsCoprime.prod_left

added theorem IsCoprime.prod_left_iff

added theorem IsCoprime.prod_right

added theorem IsCoprime.prod_right_iff

added theorem Nat.isCoprime_iff_coprime

added theorem exists_sum_eq_one_iff_pairwise_coprime'

added theorem exists_sum_eq_one_iff_pairwise_coprime

added theorem pairwise_coprime_iff_coprime_prod