Theorem IsRelPrime.add_one_left_of_dvd

Modification history

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