Int.div_pow?

Stream: Is there code for X?

[Edison Xie]

import Mathlib

example (a b : ℤ) (n : ℕ) (hxy : a ∣ b) : (a / b) ^ n = a ^ n / b ^ n := by
  sorry

Do we not have this already? I've only found Nat.div_pow :-(

[Kenny Lau]

your dvd is the wrong way

[Kenny Lau]

loogle didn't give anything

[Bhavik Mehta]

example (a b : ℤ) (n : ℕ) (hxy : b ∣ a) : (a / b) ^ n = a ^ n / b ^ n := by
  obtain ⟨c, rfl⟩ := hxy
  obtain rfl | hb := eq_or_ne b 0
  · obtain rfl | hn := eq_or_ne n 0 <;> simp [*]
  · simp [hb, mul_pow]

it does look like we don't have this...

[Eric Wieser]

A related result:

theorem Int.ediv_mul_ediv_comm {a b c d : ℤ} (hba : b ∣ a) (hdc : d ∣ c) :
    (a / b) * (c / d) = (a * c) / (b * d) := by
  obtain ⟨a, rfl⟩ := hba
  obtain ⟨c, rfl⟩ := hdc
  rw [mul_mul_mul_comm]
  obtain rfl | hb := eq_or_ne b 0; · simp
  obtain rfl | hd := eq_or_ne d 0; · simp
  simp [hb, hd]

[Edison Xie]

Kenny Lau said:

your dvd is the wrong way

oops sorry

[Edison Xie]

Bhavik Mehta said:

example (a b : ℤ) (n : ℕ) (hxy : b ∣ a) : (a / b) ^ n = a ^ n / b ^ n := by
  obtain ⟨c, rfl⟩ := hxy
  obtain rfl | hb := eq_or_ne b 0
  · obtain rfl | hn := eq_or_ne n 0 <;> simp [*]
  · simp [hb, mul_pow]

it does look like we don't have this...

Do we want it? Looks useful to have :-)

[Alex Meiburg]

Is there some kind LawfulDiv stating that when b | a, then (a / b) * b= a? Then we could state this uniformly for Nat/Int/Field (incl. Lean.Grind.Field) all in one go, as well as some version for EuclideanDomain, and maybe also Fin... also Ordinal

[Alex Meiburg]

Actually maybe docs#EuclideanDomain is almost exactly what I want, except that it doesn't support semirings (nat). It has EuclideanDomain.instDiv

[Alex Meiburg]

EuclideanDomain gets you Polynomial for free, too

[Aaron Liu]

There's docs#FloorDiv and docs#CeilDiv for the left and right adjoints of multiplication by a constant

[Edison Xie]

Bhavik Mehta said:

example (a b : ℤ) (n : ℕ) (hxy : b ∣ a) : (a / b) ^ n = a ^ n / b ^ n := by
  obtain ⟨c, rfl⟩ := hxy
  obtain rfl | hb := eq_or_ne b 0
  · obtain rfl | hn := eq_or_ne n 0 <;> simp [*]
  · simp [hb, mul_pow]

it does look like we don't have this...

#31303