Theorem IsRelPrime.add_mul_left_right_iff

Modification history

2026-05-04 16:33
Mathlib/RingTheory/Coprime/Basic.lean
feat: subtraction and ±1 lemmas for `IsCoprime, IsRelPrime` (#36948) …
Modified IsRelPrime.add_mul_left_right_iffView on Github →
2024-02-12 20:59
Mathlib/RingTheory/Coprime/Basic.lean
feat: introduce `IsRelPrime` and `DecompositionMonoid` and refactor (#10327) …
Added IsRelPrime.add_mul_left_right_iffView on Github →