where is % defined?

Stream: new members

[Jalex Stark]

# print notation % tells you about the has_mod typeclass. I'm not sure how to find the instance for \N.

[Jalex Stark]

Also are you just after the theorem nat.even_iff?

[Jalex Stark]

more generally, are you looking for these two theorems? nat.mod_eq_zero_of_dvd and nat.dvd_of_mod_eq_zero?
I found them by typing #check nat.mod_eq and then hitting ctrl-space in VSCode to see a list of completions.
(note the ctrl-space and cmd-space are two different keystrokes on macOS)

[ROCKY KAMEN-RUBIO]

Jalex Stark said:

more generally, are you looking for these two theorems? nat.mod_eq_zero_of_dvd and nat.dvd_of_mod_eq_zero?
I found them by typing #check nat.mod_eq and then hitting ctrl-space in VSCode to see a list of completions.
(note the ctrl-space and cmd-space are two different keystrokes on macOS)

I was trying to prove this thing. My approach was to start by rewriting this mod statement as algebra and then massage the algebra, but then I realized I didn't know how to rewrite a mode statement.

lemma arithmetic2 (n m d : ℕ ) (h: n ≡ m [MOD d]) (hm : m ≥ n) : ∃(k: ℕ), m = n + k * d := begin
rw nat.modeq at h,
sorry,
end

[Kevin Buzzard]

import data.nat.modeq

lemma arithmetic2 (n m d : ℕ ) (h: n ≡ m [MOD d]) (hm : m ≥ n) : ∃(k: ℕ), m = n + k * d :=
begin
  rw nat.modeq.modeq_iff_dvd' hm at h,
  cases h with k hk,
  use k,
  rwa [mul_comm, add_comm,←nat.sub_eq_iff_eq_add hm],
end

I stay away from %, I find the API for MOD much easier.

[Patrick Massot]

% is a programming thing