Commit 2025-09-23 18:22 8017dd1d

View on Github →

feat(gcongr): @[gcongr] for gcd and IsCoprime (#29889) This PR adds gcongr tags for gcd and IsCoprime. Although I don't expect it to be used very much, it is nice that we can use grw with the divisibility relation. Is the name isCoprime_mono allowed even if the relation is divisibity?

Estimated changes

modified theorem gcd_dvd_gcd_mul_left
modified theorem gcd_dvd_gcd_mul_left_right
modified theorem gcd_dvd_gcd_mul_right
modified theorem gcd_dvd_gcd_mul_right_right
added theorem IsCoprime.mono