int division of powers

Stream: Is there code for X?

[Sabbir Rahman]

Is there a theorem that says int division of powers is same as power of the subtraction? there's a version for this for Nat bases, but couldn't find any int variation

import Mathlib

example (a b c : ℕ) (hbc: b ≤ c) (ha: 0 < a) : a^c / a^b = a^(c-b) := by
  exact Nat.pow_div hbc ha

example (a: ℤ) (b c : ℕ) (hbc: b ≤ c) (ha: a ≠ 0) : a^c / a^b = a^(c-b) := by -- couldn't find thm in mathlib
  apply Int.ediv_eq_of_eq_mul_left
  . exact pow_ne_zero b ha
  . rw [← pow_add, Nat.sub_add_cancel hbc]

[Riccardo Brasca]

It seems it's not there, but we have docs#pow_sub_mul_pow that the same theorem in a certain sense

[Sabbir Rahman]

Hmm that does make it easier, still surprised at not being present, this seems fundamental enough

[Riccardo Brasca]

import Mathlib

example (a: ℤ) (b c : ℕ) (hbc: b ≤ c) (ha: a ≠ 0) : a^c / a^b = a^(c-b) := by -- couldn't find thm in mathlib
  apply mul_left_injective₀ (pow_ne_zero b ha)
  simp [Int.ediv_mul_cancel (pow_dvd_pow a hbc), pow_sub_mul_pow a hbc]

[Riccardo Brasca]

Or you can use qify

[Riccardo Brasca]

I think the idea is that it is often better to avoid integer division (we even have several versions, and I don't know exactly what / is)

[Sabbir Rahman]

yeah I know int division shouldn't really be used as most of mathematics works with real division. but I'm just surprised at the fact being missing.

[Ruben Van de Velde]

@loogle ?a ^ ?n / ?a ^ ?m

[loogle]

:search: Nat.pow_div, zpow_natCast_sub_natCast, and 24 more

[Ruben Van de Velde]

I was thinking about zpow_sub₀, but that's the other way around