Help with modular arithmetic using "sub_modEq_zero"

Stream: new members

[Kajani Kaunda]

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]

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

[Niels Voss]

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]

docs#AddCommGroup.sub_modEq_zero

[Bjørn Kjos-Hanssen]

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]

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]

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]

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