nth root operations

This file provides Real.nthRoot n to compute ⁿ√, which operates as expected on negative values when n is odd. The trap this avoids is that using rpow, (-8 : ℝ) ^ (1/3 : ℝ) = 1.

This is being upstreamed to Mathlib in leanprover-community/mathlib4#26935.

theorem SignType.pow_odd (s : SignType) (n : ℕ) (hn : Odd n) : s ^ n = s

noncomputable def Real.nthRoot (n : ℕ) (r : ℝ) : ℝ

Equations

• Real.nthRoot n r = if Even n then r ^ (↑n)⁻¹ else ↑(SignType.sign r) ^ n * |r| ^ (↑n)⁻¹

theorem Real.nthRoot_of_even {n : ℕ} (hn : Even n) (r : ℝ) : nthRoot n r = r ^ (↑n)⁻¹

theorem Real.nthRoot_of_odd {n : ℕ} (hn : Odd n) (r : ℝ) : nthRoot n r = ↑(SignType.sign r) ^ n * |r| ^ (↑n)⁻¹

theorem Real.nthRoot_of_odd_of_nonpos {n : ℕ} (hn : Odd n) {r : ℝ} (hr : r ≤ 0) : nthRoot n r = (-1) ^ n * (-r) ^ (↑n)⁻¹

theorem Real.nthRoot_of_nonneg {n : ℕ} {r : ℝ} (hr : 0 ≤ r) : nthRoot n r = r ^ (↑n)⁻¹

@[simp]

theorem Real.nthRoot_neg_of_odd {n : ℕ} (hn : Odd n) {r : ℝ} : nthRoot n (-r) = -nthRoot n r

theorem Real.pow_nthRoot {n : ℕ} (r : ℝ) (h : n ≠ 0 ∧ 0 ≤ r ∨ Odd n) : nthRoot n r ^ n = r

theorem Real.nthRoot_pow {n : ℕ} (r : ℝ) (h : n ≠ 0 ∧ 0 ≤ r ∨ Odd n) : nthRoot n (r ^ n) = r

theorem Real.nthRoot_mul_of_even_of_nonneg {n : ℕ} {a b : ℝ} (hn : Even n) (ha : 0 ≤ a) (hb : 0 ≤ b) : nthRoot n (a * b) = nthRoot n a * nthRoot n b

theorem Real.nthRoot_mul_of_odd {n : ℕ} {a b : ℝ} (hn : Odd n) : nthRoot n (a * b) = nthRoot n a * nthRoot n b