Theorem IsCoprime.add_one_sub_one_of_two_dvd

Modification history

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