getting "root" with integer power

Stream: new members

[Sabbir Rahman]

I have been trying to compile how I'd translate basic algebra proofs to lean. For power, I'm a bit stumped. There is pow_eq_pow_iff_cases that does elimination of natural power for ints, rationals, reals easily. But for integer power I feel like there should be something similar, but I can't find anything. I tried loogle but all results for ?x ^ ?y = ?z ^ ?y have nat or real power, the ones with integer power are only for LinearOrderedCommGroup, which reals or rationals aren't. Am I missing something? Or there really isn't any theorem for this?

import Mathlib

example (a b : ℝ) (n: ℤ) : a^n = b^n ↔ n = 0 ∨ a = b ∨ (a = -b ∧ Even n) := by
  sorry

[Aaron Liu]

@loogle "zpow", "inj"

[loogle]

:search: zpow_right_injective₀, zpow_right_inj₀, and 6 more

[Sabbir Rahman]

Unless I am making a mistake, all of those except two are showing equality of the integer exponents, not showing equality of the bases. The two theorems that are showing, work with LinearOrderedCommGroup which won't work for rationals or reals

[Yaël Dillies]

Yeah no we don't have these

[Eric Wieser]

I think I have Odd.zpow_right_injective somewhere

[Sabbir Rahman]

thanks for confirming, I was going crazy thinking why can't I find such a basic fact

[Yaël Dillies]

For the longest time, lemmas that were not the correct ones were taking up the correct names of the lemmas that weren't there. It was very confusing

[Sabbir Rahman]

Eric Wieser said:

I think I have Odd.zpow_right_injective somewhere

right_injective means it also proves equality of exponents, not bases?

[Eric Wieser]

I was thinking of

theorem Odd.pow_eq_pow {n : ℕ} (h : Odd n) {x y : R} : x ^ n = y ^ n ↔ x = y :=
  (@Odd.strictMono_pow R _ _ _ h).injective.eq_iff

so I guess not zpow after all

[Ilmārs Cīrulis]

Okay, I guess it is possible to prove the theorem in the original post.

import Mathlib.Analysis.Normed.Ring.Basic
import Mathlib.Data.Real.StarOrdered

theorem T0 (n: ℕ): n = 0 ∨ ∃ (p m: ℕ), n = m * 2 ^ p ∧ Odd m := by
  induction n using Nat.strong_induction_on with | h m iH =>
  obtain H | H := em (m = 0)
  . simp [H]
  . right
    obtain H0 | H0 := Nat.even_or_odd m
    . obtain ⟨w, H0⟩ := H0
      have H1: w < m := by omega
      have H2 := iH _ H1
      obtain H2 | H2 := H2
      . omega
      . obtain ⟨p, m', H2, H3⟩ := H2
        use (p + 1), m'
        simp [H3]
        subst m
        subst w
        ring_nf
    . use 0, m
      simp [H0]

theorem Odd.pow_eq_pow {n: ℕ} (h : Odd n) {x y : ℝ} : x ^ n = y ^ n ↔ x = y :=
  (@Odd.strictMono_pow ℝ _ _ _ h).injective.eq_iff

theorem T1 (a b: ℝ) (n: ℕ): a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ (a = -b ∧ Even n) := by
  constructor <;> intro H
  . obtain H0 | H0 := T0 n
    . simp [H0]
    . right
      obtain ⟨p, m, H0, H1⟩ := H0
      induction p generalizing a b n m with
      | zero =>
        simp at H0
        subst m
        rw [H1.pow_eq_pow] at H
        simp [H]
      | succ p iH =>
        have H2: n = 2 * (m * 2 ^ p) := by subst n; ring_nf
        rw [H2, pow_mul a, pow_mul b] at H
        obtain H3 | ⟨H3, H4⟩ := iH _ _ (m * 2 ^ p) H m rfl H1
        . have H4: Even n := by use (m * 2 ^ p); subst n; ring_nf
          simp [H4]
          exact sq_eq_sq_iff_eq_or_eq_neg.mp H3
        . have H5 := sq_nonneg a
          have H6 := sq_nonneg b
          have H7: a ^ 2 = 0 := by linarith
          rw [H7] at H3
          simp at *
          left
          subst a
          subst b
          rfl
  . obtain H | H | ⟨H, H0⟩ := H
    . subst n
      simp
    . subst a
      simp
    . obtain ⟨w, H0⟩ := H0
      have H1: n = 2 * w := by subst n; ring
      rw [H1]
      rw [pow_mul, pow_mul]
      subst a
      ring_nf

theorem T2 (a: ℝ) (n: ℤ) (Hn: 0 < n): a ^ n = a ^ n.toNat := by
  have H: n = Int.ofNat n.toNat := by simp; omega
  nth_rw 1 [H]
  rfl

example (a b : ℝ) (n: ℤ) : a^n = b^n ↔ n = 0 ∨ a = b ∨ (a = -b ∧ Even n) := by
  constructor <;> intro H
  . obtain H0 | H0 | H0 := Int.lt_trichotomy 0 n
    . right
      rw [T2 _ _ H0, T2 _ _ H0, T1] at H
      obtain H1 | H1 | ⟨H1, H2⟩ := H
      . omega
      . simp [H1]
      . right
        simp [H1]
        obtain ⟨w, H2⟩ := H2
        use (Int.ofNat w)
        have H3: n = Int.ofNat n.toNat := by simp; omega
        rw [H3, H2]
        simp
    . simp [H0]
    . right
      have H1: 0 < - n := by linarith
      have H2: n = (-1) * (- n) := by simp
      rw [H2, zpow_mul a, zpow_mul b] at H
      rw [T2 _ _ H1, T2 _ _ H1, T1] at H
      simp at H
      obtain H3 | H3 | ⟨H3, H4⟩ := H
      . omega
      . simp [H3]
      . rw [inv_eq_iff_eq_inv, inv_eq_one_div, inv_eq_one_div] at H3
        obtain H5 | H5 := em (b = 0)
        . subst b
          simp at H3
          simp [H3]
        . field_simp at H3
          right
          subst b
          simp
          obtain ⟨w, H4⟩ := H4
          have H6: -n = Int.ofNat (-n).toNat := by simp; omega
          have H7: Even (-n) := by rw [H6, H4]; simp
          simp at H7
          exact H7
  . obtain H | H | ⟨H, H0⟩ := H
    . subst n; simp
    . subst a; simp
    . subst a; rw [Even.neg_zpow H0 b]

[Ilmārs Cīrulis]

It was fun, nice, etc. Probably experts will use 10-50 times less lines.

[Sabbir Rahman]

@Ilmārs Cīrulis nice work. But by focusing on just the bare minimum conditions, you would've found a much shorter proof. In general the theorem needs only a LinearOrderedField and then you can "reuse" pow_eq_pow_iff_cases or similar

import Mathlib

variable {R : Type*} [LinearOrderedField R] {a b : R} {n : ℤ}

lemma zpow_eq_zpow_iff_of_ne_zero (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n :=
  match n with
  | Int.ofNat m => by
    simp only [Int.ofNat_eq_coe, ne_eq, Nat.cast_eq_zero, zpow_natCast, Int.even_coe_nat] at *
    exact pow_eq_pow_iff_of_ne_zero hn
  | Int.negSucc m => by
    rw [show Int.negSucc m = -↑(m+1) by rfl] at *
    simp only [ne_eq, neg_eq_zero, Nat.cast_eq_zero, zpow_neg, zpow_natCast, inv_inj, even_neg,
      Int.even_coe_nat] at *
    exact pow_eq_pow_iff_of_ne_zero hn

@Yaël Dillies is there any ongoing work to add the lemmas? If not I'd like to contribute to mathlib by porting a subset of https://github.com/leanprover-community/mathlib4/blob/d7c024f0292e801365f36c1ab2ba2ee2da009e32/Mathlib/Algebra/Order/Ring/Abs.lean#L206-L235 for LinearOrderedFields and integer powers

[Yaël Dillies]

It's one of the many things I would like to do, but please take it off my hands if you can!

[Yaël Dillies]

Please PR them and request my review :smile:

[Aaron Liu]

Can that be a linear ordered division semiring?

[Yaël Dillies]

Surely yes, but no one really cares about those

[Aaron Liu]

Actually, do you really need an addition?

[Aaron Liu]

The second part of the Or can be started with Associated

[Sabbir Rahman]

Aaron Liu said:

Actually, do you really need an addition?

negation is needed, is there a structure without addition but with negation? I'm not sure

[Sabbir Rahman]

Is Mathlib/Algebra/Order/Field/Power.lean a good place to put power related theorems for LinearOrderedField? I feel like yes

[Yaël Dillies]

For the time being, at least. As you see, I have started generalising many lemmas away linearly ordered fields

[Kevin Buzzard]

Sabbir Rahman said:

Aaron Liu said:

Actually, do you really need an addition?

negation is needed, is there a structure without addition but with negation? I'm not sure

Back in the day EReal had that property because negation was clear but I didn't know how to do $\infty+(-\infty)$. But now we made a choice.

[Sabbir Rahman]

Yaël Dillies said:

Please PR them and request my review :smile:

Done!! Though a test for close emoji zulip chat is failing, not sure about that