modeq_mul_cancel_left

Stream: maths

[David Renshaw]

Does mathlib have anything like this? Should it?

lemma modeq_mul_cancel_left
  (n a b c : ℕ)
  (h₁ : nat.coprime a n)
  (h₂ : a * b ≡ a * c [MOD n]) :
  b ≡ c [MOD n] :=
begin
  sorry,
end

[Adam Topaz]

We have docs#zmod.units_equiv_coprime

[Adam Topaz]

But I think going back and forth between zmod n and [MOD n] can be a pain

[Adam Topaz]

There are various variants too e.g. docs#zmod.unit_of_coprime

[David Renshaw]

Ah, I can go back and forth with https://leanprover-community.github.io/mathlib_docs/data/int/modeq.html#int.modeq.coe_nat_modeq_iff

[Adam Topaz]

Also docs#zmod.eq_iff_modeq_nat