mathlib
1494a9b2 - feat(data/zmod/basic): add `int_coe_eq_int_coe_iff_dvd_sub` (#12944)

Commit
3 years ago
feat(data/zmod/basic): add `int_coe_eq_int_coe_iff_dvd_sub` (#12944) This adds the following API lemma. ``` lemma int_coe_eq_int_coe_iff_dvd_sub (a b : ℤ) (c : ℕ) : (a : zmod c) = ↑b ↔ ↑c ∣ b-a ``` extending the already present version with b = 0. [(Zulip discussion)](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Missing.20zmod.20lemma.3F)
Parents
Loading