Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-11 06:36 8863666a

View on Github →

feat(ring_theory/ideals): prod_dvd_of_coprime (#2815)

Estimated changes

Modified src/data/polynomial.lean

added theorem polynomial.pairwise_coprime_X_sub

Created src/ring_theory/coprime.lean

added theorem finset.prod_dvd_of_coprime

added theorem fintype.prod_dvd_of_coprime

added theorem is_coprime.dvd_of_dvd_mul_left

added theorem is_coprime.dvd_of_dvd_mul_right

added theorem is_coprime.is_unit_of_dvd

added theorem is_coprime.map

added theorem is_coprime.mul_dvd

added theorem is_coprime.mul_left

added theorem is_coprime.mul_left_iff

added theorem is_coprime.mul_right

added theorem is_coprime.mul_right_iff

added theorem is_coprime.of_mul_left_left

added theorem is_coprime.of_mul_left_right

added theorem is_coprime.of_mul_right_left

added theorem is_coprime.of_mul_right_right

added theorem is_coprime.of_prod_left

added theorem is_coprime.of_prod_right

added theorem is_coprime.pow

added theorem is_coprime.pow_left

added theorem is_coprime.pow_right

added theorem is_coprime.prod_left

added theorem is_coprime.prod_left_iff

added theorem is_coprime.prod_right

added theorem is_coprime.prod_right_iff

added theorem is_coprime.symm

added def is_coprime

added theorem is_coprime_comm

added theorem is_coprime_one_left

added theorem is_coprime_one_right

added theorem is_coprime_self

added theorem is_coprime_zero_left

added theorem is_coprime_zero_right

added theorem nat.is_coprime_iff_coprime

Modified src/ring_theory/euclidean_domain.lean

Modified src/ring_theory/ideals.lean

deleted def ideal.is_coprime

deleted theorem ideal.is_coprime_def

deleted theorem ideal.is_coprime_self