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 putopen 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