Commit 2022-12-14 13:46 2d46f7bd

View on Github →

feat port: RingTheory.Coprime.Basic (#899) a95b16cbade0f938fc24abd05412bde1e84bab9b Turns out there are actually some more imports needed to port this file which were imported via tactic.ring in Lean3.

Estimated changes

added theorem IsCoprime.map
added theorem IsCoprime.mul_dvd
added theorem IsCoprime.mul_left
added theorem IsCoprime.mul_left_iff
added theorem IsCoprime.mul_right
added theorem IsCoprime.ne_zero
added theorem IsCoprime.neg_left
added theorem IsCoprime.neg_left_iff
added theorem IsCoprime.neg_neg
added theorem IsCoprime.neg_neg_iff
added theorem IsCoprime.neg_right
added theorem IsCoprime.symm
added def IsCoprime
added theorem isCoprime_comm
added theorem isCoprime_group_smul
added theorem isCoprime_one_left
added theorem isCoprime_one_right
added theorem isCoprime_self
added theorem isCoprime_zero_left
added theorem isCoprime_zero_right