exercise 4.3.4 needs extra hypothesis

Stream: Analysis I

[Rado Kirov]

The statement is

theorem zpow_add (x:ℚ) (n m:ℤ) : x^n * x^m = x^(n+m) := by sorry

but one can prove it is not actually true

example : ¬ ∀ x:ℚ, ∀ n m:ℤ, x^n * x^m = x^(n+m) := by
  push_neg
  use 0, 1, -1
  simp

How should we amend this? Two options are x \neq 0 or n + m \neq 0.

Btw, checked with — Errata to the fourth edition — https://terrytao.wordpress.com/books/analysis-i/ but didn't find anything related there.

[Aaron Liu]

@loogle "zpow_add", GroupWithZero

[loogle]

:search: zpow_add_one₀, zpow_add₀, and 1 more

[Aaron Liu]

You can try copying the signature of one of those results

[Terence Tao]

Ah, I omitted the hypothesis x ≠ 0 from the Lean exercise; I checked the book and the hypothesis is stated explicitly. Please feel free to submit an appropriate PR to fix this (and any other fixes or tips you have found as well)!

[Rado Kirov]

Oh, I missed it too because it was in the general exercise text, not just a), but b-d) have local strengthening or don't need it. Will send a PR shortly