FormalConjecturesForMathlib.Analysis.SpecialFunctions.NthRoot

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module


public import Mathlib.Analysis.SpecialFunctions.Pow.Real

@[expose] public section

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.

namespace Real

noncomputable def nthRoot (n : ℕ) (r : ℝ) : ℝ :=
  if Even n then r ^ (n⁻¹ : ℝ) else SignType.sign r ^ n * abs r ^ (n⁻¹ : ℝ)

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

theorem nthRoot_of_odd {n : ℕ} (hn : Odd n) (r : ℝ) :
    nthRoot n r = SignType.sign r ^ n * abs r ^ (n⁻¹ : ℝ) :=
  if_neg <| Nat.not_even_iff_odd.mpr hn



theorem nthRoot_of_odd_of_nonpos {n : ℕ} (hn : Odd n) {r : ℝ} (hr : r ≤ 0) :
    nthRoot n r = (-1) ^ n * (-r) ^ (n⁻¹ : ℝ) := byn:ℕhn:Odd nr:ℝhr:r ≤ 0⊢ nthRoot n r = (-1) ^ n * (-r) ^ (↑n)⁻¹
  rw [nthRoot_of_odd hnn:ℕhn:Odd nr:ℝhr:r ≤ 0⊢ ↑(SignType.sign r) ^ n * |r| ^ (↑n)⁻¹ = (-1) ^ n * (-r) ^ (↑n)⁻¹n:ℕhn:Odd nr:ℝhr:r ≤ 0⊢ ↑(SignType.sign r) ^ n * |r| ^ (↑n)⁻¹ = (-1) ^ n * (-r) ^ (↑n)⁻¹]n:ℕhn:Odd nr:ℝhr:r ≤ 0⊢ ↑(SignType.sign r) ^ n * |r| ^ (↑n)⁻¹ = (-1) ^ n * (-r) ^ (↑n)⁻¹
  obtain rfl | hr := hr.eq_or_ltinln:ℕhn:Odd nhr:0 ≤ 0⊢ ↑(SignType.sign 0) ^ n * |0| ^ (↑n)⁻¹ = (-1) ^ n * (-0) ^ (↑n)⁻¹inrn:ℕhn:Odd nr:ℝhr✝:r ≤ 0hr:r < 0⊢ ↑(SignType.sign r) ^ n * |r| ^ (↑n)⁻¹ = (-1) ^ n * (-r) ^ (↑n)⁻¹
  ·inln:ℕhn:Odd nhr:0 ≤ 0⊢ ↑(SignType.sign 0) ^ n * |0| ^ (↑n)⁻¹ = (-1) ^ n * (-0) ^ (↑n)⁻¹ simpinln:ℕhn:Odd nhr:0 ≤ 0⊢ 0 ^ n = (-1) ^ n ∨ 0 ^ (↑n)⁻¹ = 0
    have hn0 : n ≠ 0 := Nat.ne_of_odd_add hninln:ℕhn:Odd nhr:0 ≤ 0hn0:n ≠ 0⊢ 0 ^ n = (-1) ^ n ∨ 0 ^ (↑n)⁻¹ = 0
    rw [zero_pow hn0,inln:ℕhn:Odd nhr:0 ≤ 0hn0:n ≠ 0⊢ 0 = (-1) ^ n ∨ 0 ^ (↑n)⁻¹ = 0inln:ℕhn:Odd nhr:0 ≤ 0hn0:n ≠ 0⊢ 0 = (-1) ^ n ∨ 0 = 0 zero_rpow (inv_ne_zero <| mod_cast hn0)inln:ℕhn:Odd nhr:0 ≤ 0hn0:n ≠ 0⊢ 0 = (-1) ^ n ∨ 0 = 0inln:ℕhn:Odd nhr:0 ≤ 0hn0:n ≠ 0⊢ 0 = (-1) ^ n ∨ 0 = 0]inln:ℕhn:Odd nhr:0 ≤ 0hn0:n ≠ 0⊢ 0 = (-1) ^ n ∨ 0 = 0
    rightinln:ℕhn:Odd nhr:0 ≤ 0hn0:n ≠ 0⊢ 0 = 0
    rflAll goals completed! 🐙
  ·inrn:ℕhn:Odd nr:ℝhr✝:r ≤ 0hr:r < 0⊢ ↑(SignType.sign r) ^ n * |r| ^ (↑n)⁻¹ = (-1) ^ n * (-r) ^ (↑n)⁻¹ rw [abs_of_neg hr,inrn:ℕhn:Odd nr:ℝhr✝:r ≤ 0hr:r < 0⊢ ↑(SignType.sign r) ^ n * (-r) ^ (↑n)⁻¹ = (-1) ^ n * (-r) ^ (↑n)⁻¹inrn:ℕhn:Odd nr:ℝhr✝:r ≤ 0hr:r < 0⊢ ↑(-1) ^ n * (-r) ^ (↑n)⁻¹ = (-1) ^ n * (-r) ^ (↑n)⁻¹ _root_.sign_neg hrinrn:ℕhn:Odd nr:ℝhr✝:r ≤ 0hr:r < 0⊢ ↑(-1) ^ n * (-r) ^ (↑n)⁻¹ = (-1) ^ n * (-r) ^ (↑n)⁻¹inrn:ℕhn:Odd nr:ℝhr✝:r ≤ 0hr:r < 0⊢ ↑(-1) ^ n * (-r) ^ (↑n)⁻¹ = (-1) ^ n * (-r) ^ (↑n)⁻¹]inrn:ℕhn:Odd nr:ℝhr✝:r ≤ 0hr:r < 0⊢ ↑(-1) ^ n * (-r) ^ (↑n)⁻¹ = (-1) ^ n * (-r) ^ (↑n)⁻¹
    simpAll goals completed! 🐙



theorem nthRoot_of_nonneg {n : ℕ} {r : ℝ} (hr : 0 ≤ r) :
    nthRoot n r = r ^ (n⁻¹ : ℝ) := byn:ℕr:ℝhr:0 ≤ r⊢ nthRoot n r = r ^ (↑n)⁻¹
  cases Nat.even_or_odd n with
  | inl he =>inln:ℕr:ℝhr:0 ≤ rhe:Even n⊢ nthRoot n r = r ^ (↑n)⁻¹
    rw [nthRoot_of_even heinln:ℕr:ℝhr:0 ≤ rhe:Even n⊢ r ^ (↑n)⁻¹ = r ^ (↑n)⁻¹All goals completed! 🐙]All goals completed! 🐙
  | inr ho =>inrn:ℕr:ℝhr:0 ≤ rho:Odd n⊢ nthRoot n r = r ^ (↑n)⁻¹
    have hn0 : n ≠ 0 := Nat.ne_of_odd_add hoinrn:ℕr:ℝhr:0 ≤ rho:Odd nhn0:n ≠ 0⊢ nthRoot n r = r ^ (↑n)⁻¹
    rw [nthRoot_of_odd ho,inrn:ℕr:ℝhr:0 ≤ rho:Odd nhn0:n ≠ 0⊢ ↑(SignType.sign r) ^ n * |r| ^ (↑n)⁻¹ = r ^ (↑n)⁻¹inrn:ℕr:ℝhr:0 ≤ rho:Odd nhn0:n ≠ 0⊢ ↑(SignType.sign r) ^ n * r ^ (↑n)⁻¹ = r ^ (↑n)⁻¹ abs_of_nonneg hrinrn:ℕr:ℝhr:0 ≤ rho:Odd nhn0:n ≠ 0⊢ ↑(SignType.sign r) ^ n * r ^ (↑n)⁻¹ = r ^ (↑n)⁻¹inrn:ℕr:ℝhr:0 ≤ rho:Odd nhn0:n ≠ 0⊢ ↑(SignType.sign r) ^ n * r ^ (↑n)⁻¹ = r ^ (↑n)⁻¹]inrn:ℕr:ℝhr:0 ≤ rho:Odd nhn0:n ≠ 0⊢ ↑(SignType.sign r) ^ n * r ^ (↑n)⁻¹ = r ^ (↑n)⁻¹
    obtain rfl | hr := hr.eq_or_ltinr.inln:ℕho:Odd nhn0:n ≠ 0hr:0 ≤ 0⊢ ↑(SignType.sign 0) ^ n * 0 ^ (↑n)⁻¹ = 0 ^ (↑n)⁻¹inr.inrn:ℕr:ℝhr✝:0 ≤ rho:Odd nhn0:n ≠ 0hr:0 < r⊢ ↑(SignType.sign r) ^ n * r ^ (↑n)⁻¹ = r ^ (↑n)⁻¹
    ·inr.inln:ℕho:Odd nhn0:n ≠ 0hr:0 ≤ 0⊢ ↑(SignType.sign 0) ^ n * 0 ^ (↑n)⁻¹ = 0 ^ (↑n)⁻¹ simp [hn0]All goals completed! 🐙
    rw [_root_.sign_pos hrinr.inrn:ℕr:ℝhr✝:0 ≤ rho:Odd nhn0:n ≠ 0hr:0 < r⊢ ↑1 ^ n * r ^ (↑n)⁻¹ = r ^ (↑n)⁻¹inr.inrn:ℕr:ℝhr✝:0 ≤ rho:Odd nhn0:n ≠ 0hr:0 < r⊢ ↑1 ^ n * r ^ (↑n)⁻¹ = r ^ (↑n)⁻¹]inr.inrn:ℕr:ℝhr✝:0 ≤ rho:Odd nhn0:n ≠ 0hr:0 < r⊢ ↑1 ^ n * r ^ (↑n)⁻¹ = r ^ (↑n)⁻¹
    simpAll goals completed! 🐙



@[simp]
theorem nthRoot_neg_of_odd {n : ℕ} (hn : Odd n) {r : ℝ} :
    nthRoot n (-r) = -nthRoot n r := byn:ℕhn:Odd nr:ℝ⊢ nthRoot n (-r) = -nthRoot n r
  obtain hr | hr := le_total r 0inln:ℕhn:Odd nr:ℝhr:r ≤ 0⊢ nthRoot n (-r) = -nthRoot n rinrn:ℕhn:Odd nr:ℝhr:0 ≤ r⊢ nthRoot n (-r) = -nthRoot n r
  ·inln:ℕhn:Odd nr:ℝhr:r ≤ 0⊢ nthRoot n (-r) = -nthRoot n r rw [nthRoot_of_odd_of_nonpos hn hr,inln:ℕhn:Odd nr:ℝhr:r ≤ 0⊢ nthRoot n (-r) = -((-1) ^ n * (-r) ^ (↑n)⁻¹)All goals completed! 🐙 hn.neg_one_pow,inln:ℕhn:Odd nr:ℝhr:r ≤ 0⊢ nthRoot n (-r) = -(-1 * (-r) ^ (↑n)⁻¹)All goals completed! 🐙 neg_one_mul,inln:ℕhn:Odd nr:ℝhr:r ≤ 0⊢ nthRoot n (-r) = - -(-r) ^ (↑n)⁻¹All goals completed! 🐙 neg_neg,inln:ℕhn:Odd nr:ℝhr:r ≤ 0⊢ nthRoot n (-r) = (-r) ^ (↑n)⁻¹All goals completed! 🐙
      nthRoot_of_nonneg (neg_nonneg.mpr hr)inln:ℕhn:Odd nr:ℝhr:r ≤ 0⊢ (-r) ^ (↑n)⁻¹ = (-r) ^ (↑n)⁻¹All goals completed! 🐙]All goals completed! 🐙
  ·inrn:ℕhn:Odd nr:ℝhr:0 ≤ r⊢ nthRoot n (-r) = -nthRoot n r rw [nthRoot_of_odd_of_nonpos hn (neg_nonpos.mpr hr),inrn:ℕhn:Odd nr:ℝhr:0 ≤ r⊢ (-1) ^ n * (- -r) ^ (↑n)⁻¹ = -nthRoot n rAll goals completed! 🐙 hn.neg_one_pow,inrn:ℕhn:Odd nr:ℝhr:0 ≤ r⊢ -1 * (- -r) ^ (↑n)⁻¹ = -nthRoot n rAll goals completed! 🐙 neg_one_mul,inrn:ℕhn:Odd nr:ℝhr:0 ≤ r⊢ -(- -r) ^ (↑n)⁻¹ = -nthRoot n rAll goals completed! 🐙 neg_neg,inrn:ℕhn:Odd nr:ℝhr:0 ≤ r⊢ -r ^ (↑n)⁻¹ = -nthRoot n rAll goals completed! 🐙
      nthRoot_of_nonneg hrinrn:ℕhn:Odd nr:ℝhr:0 ≤ r⊢ -r ^ (↑n)⁻¹ = -r ^ (↑n)⁻¹All goals completed! 🐙]All goals completed! 🐙



theorem pow_nthRoot {n : ℕ} (r : ℝ) (h : (n ≠ 0 ∧ 0 ≤ r) ∨ Odd n) : nthRoot n r ^ n = r := byn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd n⊢ nthRoot n r ^ n = r
  cases Nat.even_or_odd n with
  | inl he =>inln:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nhe:Even n⊢ nthRoot n r ^ n = r
    obtain ⟨hn, hr⟩ := h.resolve_right (Nat.not_odd_iff_even.mpr he)inln:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nhe:Even nhn:n ≠ 0hr:0 ≤ r⊢ nthRoot n r ^ n = r
    rw [nthRoot_of_even he,inln:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nhe:Even nhn:n ≠ 0hr:0 ≤ r⊢ (r ^ (↑n)⁻¹) ^ n = rAll goals completed! 🐙 rpow_inv_natCast_pow hr hninln:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nhe:Even nhn:n ≠ 0hr:0 ≤ r⊢ r = rAll goals completed! 🐙]All goals completed! 🐙
  | inr ho =>inrn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd n⊢ nthRoot n r ^ n = r
    have hn : n ≠ 0 := by exact Nat.ne_of_odd_add hoinrn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ nthRoot n r ^ n = rinrn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ nthRoot n r ^ n = r
    rw [nthRoot_of_odd ho,inrn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ (↑(SignType.sign r) ^ n * |r| ^ (↑n)⁻¹) ^ n = rinr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n) mul_pow,inrn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ (↑(SignType.sign r) ^ n) ^ n * (|r| ^ (↑n)⁻¹) ^ n = rinr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n) ←pow_mul,inrn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ ↑(SignType.sign r) ^ (n * n) * (|r| ^ (↑n)⁻¹) ^ n = rinr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n) rpow_inv_natCast_pow (abs_nonneg _) hn,inrn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ ↑(SignType.sign r) ^ (n * n) * |r| = rinr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n)
      ←SignType.coe_pow,inrn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ ↑(SignType.sign r ^ (n * n)) * |r| = rinr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n) SignType.pow_odd,inrn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ ↑(SignType.sign r) * |r| = rinr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n)inr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n) sign_mul_absinrn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ r = rinr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n)inr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n)]inr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n)
    exact ho.mul hoAll goals completed! 🐙



theorem nthRoot_pow {n : ℕ} (r : ℝ) (h : (n ≠ 0 ∧ 0 ≤ r) ∨ Odd n) : nthRoot n (r ^ n) = r := byn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd n⊢ nthRoot n (r ^ n) = r
  cases Nat.even_or_odd n with
  | inl he =>inln:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nhe:Even n⊢ nthRoot n (r ^ n) = r
    obtain ⟨hn, hr⟩ := h.resolve_right (Nat.not_odd_iff_even.mpr he)inln:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nhe:Even nhn:n ≠ 0hr:0 ≤ r⊢ nthRoot n (r ^ n) = r
    rw [nthRoot_of_even he,inln:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nhe:Even nhn:n ≠ 0hr:0 ≤ r⊢ (r ^ n) ^ (↑n)⁻¹ = rAll goals completed! 🐙 pow_rpow_inv_natCast hr hninln:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nhe:Even nhn:n ≠ 0hr:0 ≤ r⊢ r = rAll goals completed! 🐙]All goals completed! 🐙
  | inr ho =>inrn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd n⊢ nthRoot n (r ^ n) = r
    have hn : n ≠ 0 := Nat.ne_of_odd_add hoinrn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ nthRoot n (r ^ n) = r
    rw [nthRoot_of_odd ho,inrn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ ↑(SignType.sign (r ^ n)) ^ n * |r ^ n| ^ (↑n)⁻¹ = rinr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n) abs_pow,inrn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ ↑(SignType.sign (r ^ n)) ^ n * (|r| ^ n) ^ (↑n)⁻¹ = rinr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n) pow_rpow_inv_natCast (abs_nonneg _) hn,inrn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ ↑(SignType.sign (r ^ n)) ^ n * |r| = rinr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n)
      ←SignType.coe_pow,inrn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ ↑(SignType.sign (r ^ n) ^ n) * |r| = rinr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n) sign_pow,inrn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ ↑((SignType.sign r ^ n) ^ n) * |r| = rinr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n) ← pow_mul,inrn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ ↑(SignType.sign r ^ (n * n)) * |r| = rinr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n) SignType.pow_odd,inrn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ ↑(SignType.sign r) * |r| = rinr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n)inr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n) sign_mul_absinrn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ r = rinr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n)inr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n)]inr.hnn:ℕr:ℝh:n ≠ 0 ∧ 0 ≤ r ∨ Odd nho:Odd nhn:n ≠ 0⊢ Odd (n * n)
    exact ho.mul hoAll goals completed! 🐙

theorem nthRoot_mul_of_even_of_nonneg {n : ℕ} {a b : ℝ} (hn : Even n)
    (ha : 0 ≤ a) (hb : 0 ≤ b) :
    Real.nthRoot n (a * b) = Real.nthRoot n a * Real.nthRoot n b := byn:ℕa:ℝb:ℝhn:Even nha:0 ≤ ahb:0 ≤ b⊢ nthRoot n (a * b) = nthRoot n a * nthRoot n b
  simp only [Real.nthRoot_of_even hn, Real.mul_rpow ha hb]All goals completed! 🐙

theorem nthRoot_mul_of_odd {n : ℕ} {a b : ℝ} (hn : Odd n) :
    nthRoot n (a * b) = nthRoot n a * nthRoot n b := byn:ℕa:ℝb:ℝhn:Odd n⊢ nthRoot n (a * b) = nthRoot n a * nthRoot n b
  simp [Real.nthRoot_of_odd hn, sign_mul, SignType.coe_mul, abs_mul,
  Real.mul_rpow (abs_nonneg a) (abs_nonneg b)]n:ℕa:ℝb:ℝhn:Odd n⊢ (↑(SignType.sign a) * ↑(SignType.sign b)) ^ n * (|a| ^ (↑n)⁻¹ * |b| ^ (↑n)⁻¹) =
  ↑(SignType.sign a) ^ n * |a| ^ (↑n)⁻¹ * (↑(SignType.sign b) ^ n * |b| ^ (↑n)⁻¹)
  ringAll goals completed! 🐙

end Real