FormalConjecturesForMathlib/Analysis/SpecialFunctions/NthRoot.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

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.

Imports (1)
Imported by 1 file
  1. def Real.nthRoot line 35 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real

    Proof uses: ite, Even, HPow.hPow, Inv.inv, HMul.hMul, OrderHom, SignType, SignType.sign, abs

    28 instances, coercions and auxiliary constants left out.

  2. theorem Real.nthRoot_of_even line 38 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Even, Real, Eq, Real.nthRoot, HPow.hPow, Inv.inv

    Proof uses: if_pos, HMul.hMul, OrderHom, SignType, SignType.sign, abs

    34 instances, coercions and auxiliary constants left out.

  3. theorem Real.nthRoot_of_odd line 41 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Odd, Real, Eq, Real.nthRoot, HMul.hMul, HPow.hPow, OrderHom, SignType, SignType.sign, abs, Inv.inv

    Proof uses: if_neg, Even, Iff.mpr, Not, Nat.not_even_iff_odd

    56 instances, coercions and auxiliary constants left out.

  4. theorem Real.nthRoot_of_odd_of_nonpos line 45 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Odd, Real, LE.le, OfNat.ofNat, Eq, Real.nthRoot, HMul.hMul, HPow.hPow, Neg.neg, Inv.inv

    Proof uses: Eq.mpr, OrderHom, SignType, SignType.sign, abs, id, congrArg, Real.nthRoot_of_odd, LT.lt, Or, LE.le.eq_or_lt, Eq.trans, congr, congrFun', sign_zero, abs_zero, neg_zero, Ne, Nat.ne_of_odd_add, zero_pow and 14 more

    99 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

    Open to load the checked before-and-after goal states.

  5. theorem Real.nthRoot_of_nonneg line 57 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, LE.le, OfNat.ofNat, Eq, Real.nthRoot, HPow.hPow, Inv.inv

    Proof uses: Even, Odd, Or, Nat.even_or_odd, Or.inl, Eq.mpr, id, congrArg, Real.nthRoot_of_even, Eq.refl, Or.inr, Ne, Nat.ne_of_odd_add, HMul.hMul, OrderHom, SignType, SignType.sign, abs, Real.nthRoot_of_odd, abs_of_nonneg and 19 more

    84 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

    Open to load the checked before-and-after goal states.

  6. theorem Real.nthRoot_neg_of_odd line 71 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Odd, Real, Eq, Real.nthRoot, Neg.neg

    Proof uses: LE.le, OfNat.ofNat, Or, le_total, Eq.mpr, HMul.hMul, HPow.hPow, Inv.inv, id, congrArg, Real.nthRoot_of_odd_of_nonpos, Odd.neg_one_pow, neg_one_mul, neg_neg, Real.nthRoot_of_nonneg, Iff.mpr, neg_nonneg, Eq.refl, neg_nonpos

    51 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

  7. theorem Real.pow_nthRoot line 79 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, Or, And, Ne, OfNat.ofNat, LE.le, Odd, Eq, HPow.hPow, Real.nthRoot

    Proof uses: Even, Nat.even_or_odd, Or.inl, Or.resolve_right, Iff.mpr, Not, Nat.not_odd_iff_even, Eq.mpr, Inv.inv, id, congrArg, Real.nthRoot_of_even, Real.rpow_inv_natCast_pow, Eq.refl, Or.inr, Nat.ne_of_odd_add, HMul.hMul, OrderHom, SignType, SignType.sign and 10 more

    88 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

    Open to load the checked before-and-after goal states.

  8. theorem Real.nthRoot_pow line 90 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, Or, And, Ne, OfNat.ofNat, LE.le, Odd, Eq, Real.nthRoot, HPow.hPow

    Proof uses: Even, Nat.even_or_odd, Or.inl, Or.resolve_right, Iff.mpr, Not, Nat.not_odd_iff_even, Eq.mpr, Inv.inv, id, congrArg, Real.nthRoot_of_even, Real.pow_rpow_inv_natCast, Eq.refl, Or.inr, Nat.ne_of_odd_add, HMul.hMul, OrderHom, SignType, SignType.sign and 11 more

    86 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

    Open to load the checked before-and-after goal states.

  9. theorem Real.nthRoot_mul_of_even_of_nonneg line 101 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, Even, LE.le, OfNat.ofNat, Eq, Real.nthRoot, HMul.hMul

    Proof uses: of_eq_true, Eq.trans, HPow.hPow, Inv.inv, True, congr, congrArg, Real.nthRoot_of_even, Real.mul_rpow, eq_self

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  10. theorem Real.nthRoot_mul_of_odd line 106 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, Odd, Eq, Real.nthRoot, HMul.hMul

    Proof uses: Eq.mpr, HPow.hPow, OrderHom, SignType, SignType.sign, abs, Inv.inv, id, congr, congrArg, Eq.trans, Real.nthRoot_of_odd, congrFun', sign_mul, SignType.coe_mul, abs_mul, Real.mul_rpow, abs_nonneg, LE.le, Mathlib.Tactic.Ring.of_eq and 25 more

    76 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.