## Stream: general

### Topic: hole? golf!

#### Johan Commelin (Apr 21 2020 at 12:10):

Is this a hole in the library? What is the shortest proof?

lemma dvd_sub_mod (k : ℕ) : n ∣ (k - (k % n)) :=


#### Kenny Lau (Apr 21 2020 at 12:14):

lemma dvd_sub_mod (n k : ℕ) : n ∣ (k - (k % n)) :=


#### Mario Carneiro (Apr 21 2020 at 12:16):

lemma dvd_sub_mod (n k : ℕ) : n ∣ k - k % n :=
⟨k / n, (nat.sub_eq_iff_eq_add (nat.mod_le _ _)).2 \$


#### Kenny Lau (Apr 21 2020 at 12:16):

yay my proof is shorter

#### Mario Carneiro (Apr 21 2020 at 12:18):

Damn you autocomplete
Screenshot-from-2020-04-21-05-17-09.png

#### Kenny Lau (Apr 21 2020 at 12:19):

looks like you have no imports?

#### Mario Carneiro (Apr 21 2020 at 12:19):

Oh, yes import data.nat.basic solves the problem

#### Reid Barton (Apr 21 2020 at 12:21):

The nat subtraction makes this annoying.

lemma dvd_sub_mod (n k : ℤ) : n ∣ (k - (k % n)) :=
int.modeq.modeq_iff_dvd.mp (int.modeq.mod_modeq _ _)


#### Bhavik Mehta (Apr 21 2020 at 12:21):

Mario Carneiro said:

Damn you autocomplete
Screenshot-from-2020-04-21-05-17-09.png

(entirely unrelated - which theme is this? I quite like it)

night owl

name checks out

cheater

#### Reid Barton (Apr 21 2020 at 12:24):

maybe another hole is, in data.nat.modeq:

theorem modeq_iff_dvd_of_le (a ≤ b) : a ≡ b [MOD n] ↔ n ∣ b - a


#### Mario Carneiro (Apr 21 2020 at 12:24):

I like the statement golfing

#### Reid Barton (Apr 21 2020 at 12:25):

removed an extraneous space to make it shorter

#### Mario Carneiro (Apr 21 2020 at 12:26):

I would skip the of_le in the name

#### Mario Carneiro (Apr 21 2020 at 12:26):

unless you want another version when it's not of_le

#### Kenny Lau (Apr 21 2020 at 12:27):

The nonunits make this annoying.

import ring_theory.euclidean_domain data.real.basic

lemma dvd_sub_mod (n k : ℝ) : n ∣ (k - (k % n)) :=
if H : n = 0 then by rw [H, euclidean_domain.mod_zero, sub_self]
else ⟨(k - k % n) / n, by rw mul_div_cancel' _ H⟩


#### Reid Barton (Apr 21 2020 at 12:27):

There's an existing theorem modeq_iff_dvd : a ≡ b [MOD n] ↔ (n:ℤ) ∣ b - a but maybe that should be the one with the altered name

#### Mario Carneiro (Apr 21 2020 at 12:28):

Yeah but that's in a different namespace, right?

#### Mario Carneiro (Apr 21 2020 at 12:29):

Oh I see this is for nats

#### Reid Barton (Apr 21 2020 at 12:29):

No this is for nats (MOD is for nat)--there's also theorem modeq_iff_dvd : a ≡ b [ZMOD n] ↔ (n:ℤ) ∣ b - a := in int.zmod

Last updated: May 16 2021 at 21:11 UTC