Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-01 15:54 249a015c

View on Github →

chore(ring_theory/coprime): split out imports into a new file so that is_coprime can be used earlier. (#9403) Zulip

Estimated changes

Modified src/data/polynomial/field_division.lean

Modified src/number_theory/fermat4.lean

Renamed src/ring_theory/coprime.lean to src/ring_theory/coprime/basic.lean

deleted theorem finset.prod_dvd_of_coprime

deleted theorem fintype.prod_dvd_of_coprime

deleted theorem is_coprime.of_prod_left

deleted theorem is_coprime.of_prod_right

deleted theorem is_coprime.pow

deleted theorem is_coprime.pow_iff

deleted theorem is_coprime.pow_left

deleted theorem is_coprime.pow_left_iff

deleted theorem is_coprime.pow_right

deleted theorem is_coprime.pow_right_iff

deleted theorem is_coprime.prod_left

deleted theorem is_coprime.prod_left_iff

deleted theorem is_coprime.prod_right

deleted theorem is_coprime.prod_right_iff

deleted theorem nat.is_coprime_iff_coprime

Created src/ring_theory/coprime/lemmas.lean

added theorem finset.prod_dvd_of_coprime

added theorem fintype.prod_dvd_of_coprime

added theorem is_coprime.of_prod_left

added theorem is_coprime.of_prod_right

added theorem is_coprime.pow

added theorem is_coprime.pow_iff

added theorem is_coprime.pow_left

added theorem is_coprime.pow_left_iff

added theorem is_coprime.pow_right

added theorem is_coprime.pow_right_iff

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 nat.is_coprime_iff_coprime

Modified src/ring_theory/euclidean_domain.lean

Modified src/ring_theory/int/basic.lean