how far to go with junk theorem

Stream: general

[Kevin Buzzard]

If noncomputable definition nth_root (x : ℝ) (n : ℕ) : ℝ := exp (log x / n) then because log of a non-positive real is explicitly defined to be zero (log going out of its way to not ask for positivity there), we have that

lemma nth_root_pow_left' {x : ℝ} {m n : ℕ} (Hn : 0 < n) : --(Hm : 0 < m) (Hx : 0 < x) :
(nth_root x (m * n)) ^ n = nth_root x m := sorry

happens to be true for all m and x. However to prove the result for x <= 0 I would like to use the fact that if x <= 0 then log x = 0. Should this be a named lemma, even though it's a junk theorem? I can't find it.

[Kevin Buzzard]

Am I supposed to put the effort in to prove the result for x<=0 even though nobody will ever need this case?

[Mario Carneiro]

yes to both questions

[Mario Carneiro]

If you use the fact at least once, there should be a theorem describing "out of domain" behavior of a totalized function (although in general we want to limit the number of such theorems)

[Mario Carneiro]

and if it eliminates a hypothesis you should use "out of domain" behavior of functions in the proof