mod_pow_mod

Stream: Is there code for X?

[Aaron Bies]

Does the mathlib already have a version of this and if not, should we add one?

lemma mod_pow_mod (a b n : ℕ) :
  (a % n) ^ b % n = a ^ b % n :=
begin
  induction b with b ih,
  refl, simp [pow_succ, nat.mul_mod, ih],
end

-- example use case (first semester exam question)
example (n : ℕ) : 6 ∣ 7 ^ n + 11 :=
begin
  rw [nat.dvd_iff_mod_eq_zero, nat.add_mod, ←mod_pow_mod],
  change (1 ^ n % 6 + 5) % 6 = 0,
  rw one_pow, refl,
end

[Eric Wieser]

It's tempting to state it in reverse as nat.pow_mod to match docs#nat.mul_mod

[Eric Wieser]

I don't think we have it

[Aaron Bies]

I agree it's probably more useful in reverse

[Aaron Bies]

The name pow_mod feels a little vague to me, but I guess it matches similar theorems pretty well

[Eric Wieser]

It should be nat.pow_mod

[Eric Wieser]

Note that this matches the #naming guide, since the LHS of the reversed expression, (a ^ b) % n, is mod with pow as its left argument

[Eric Wieser]

Want to PR it?

[Aaron Bies]

Alright, I'll set up the PR

[Aaron Bies]

https://github.com/leanprover-community/mathlib/pull/13550 (I hope I'm doing this right)

[Kevin Buzzard]

Unfortunately you're not :-) We only accept PRs from non-master branches of the project, rather than from forks, because of issues related to CI. @maintainers can github user slerpyyy have push access to non-master branches of mathlib? Aaron can you close the PR and make a new one once you can push to a branch?

[Kevin Buzzard]

Here's the documentation on the procedure: https://leanprover-community.github.io/contribute/index.html Thanks for making the PR!

[Bryan Gin-ge Chen]

Invite sent! https://github.com/leanprover-community/mathlib/invitations

[Aaron Bies]

Ah, sorry, I should have read the guide first

[Aaron Bies]

Give me a moment to clean up this mess and try again

[Aaron Bies]

Second attempt: https://github.com/leanprover-community/mathlib/pull/13551

[Jireh Loreaux]

FYI: you can type #13551 to get #13551