Zulip Chat Archive

Stream: maths

Topic: modeq_mul_cancel_left


David Renshaw (May 16 2021 at 14:03):

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 (May 16 2021 at 14:21):

We have docs#zmod.units_equiv_coprime

Adam Topaz (May 16 2021 at 14:22):

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

Adam Topaz (May 16 2021 at 14:25):

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

David Renshaw (May 16 2021 at 14:30):

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 (May 16 2021 at 14:39):

Also docs#zmod.eq_iff_modeq_nat


Last updated: Dec 20 2023 at 11:08 UTC