Zulip Chat Archive

Stream: new members

Topic: Help with modular arithmetic using "sub_modEq_zero"


Kajani Kaunda (Sep 25 2024 at 17:42):

Hello,

given the following theorems defined in import Mathlib.Algebra.ModEq

theorem sub_modEq_iff_modEq_add : a - b  c [PMOD p]  a  c + b [PMOD p] :=
  modEq_comm.trans <| modEq_sub_iff_add_modEq.trans modEq_comm

@[simp]
theorem sub_modEq_zero : a - b  0 [PMOD p]  a  b [PMOD p] := by simp [sub_modEq_iff_modEq_add]

how do we solve this example?

example (p : ) (h0 : p  2 [MOD 6]) : p - 2  0 [MOD 6] := sorry

this is my attempt which gives the error: "unknown identifier 'sub_modEq_zero'"

import Mathlib.Algebra.ModEq

example (p : ) (h0 : p  2 [MOD 6]) : p - 2  0 [MOD 6] := by simp [sub_modEq_zero, h0]

Niels Voss (Sep 25 2024 at 18:49):

Just a hunch but are you sure sub_modEq_zero isn't in a namespace?

Niels Voss (Sep 25 2024 at 18:52):

It seems to be AddCommGroup.sub_modEq_zero. I think you either need to write out the full name with the namespace or put open AddCommGroup somewhere above your definition

Niels Voss (Sep 25 2024 at 18:53):

docs#AddCommGroup.sub_modEq_zero

Bjørn Kjos-Hanssen (Sep 25 2024 at 18:54):

This works:

import Mathlib.Algebra.ModEq

example (p : ) (h0 : p  2 [PMOD 6]) : p - 2  0 [PMOD 6] := AddCommGroup.sub_modEq_zero.mpr h0

Kajani Kaunda (Sep 25 2024 at 20:00):

Niels Voss said:

It seems to be AddCommGroup.sub_modEq_zero. I think you either need to write out the full name with the namespace or put open AddCommGroup somewhere above your definition

Thanks, I will try that out ...

Kajani Kaunda (Sep 25 2024 at 20:16):

Bjørn Kjos-Hanssen ☀️ said:

This works:

import Mathlib.Algebra.ModEq

example (p : ) (h0 : p  2 [PMOD 6]) : p - 2  0 [PMOD 6] := AddCommGroup.sub_modEq_zero.mpr h0

This works indeed! Thank you so much! It turns out that a key thing to watch out for is the difference between integer arithmetic () and natural number arithmetic () in Lean - the hypothesis (p : Nat) is not compatible with the theorem sub_modEq_zero.

Kajani Kaunda (Sep 25 2024 at 20:21):

Thank you all for the help, it is much appreciated.


Last updated: May 02 2025 at 03:31 UTC