Theorem IsRelPrime.mul_sub_left_right_iff

Modification history

2026-05-04 16:33
Mathlib/RingTheory/Coprime/Basic.lean
feat: subtraction and ±1 lemmas for `IsCoprime, IsRelPrime` (#36948) …
Added IsRelPrime.mul_sub_left_right_iffView on Github →