Documentation Verification Report

NthRootLemmas

📁 Source: Mathlib/Analysis/SpecialFunctions/Pow/NthRootLemmas.lean

Statistics

Metric	Count
Definitions `instDecidableExistsPowEq`	1
Theorems `exists_pow_eq_iff`, `exists_pow_eq_iff'`, `le_nthRoot_iff`, `lt_pow_nthRoot_add_one`, `lt_pow_go_succ_aux`, `nthRoot_eq_of_le_of_lt`, `nthRoot_lt_iff`, `nthRoot_one_left`, `nthRoot_one_right`, `nthRoot_pow`, `nthRoot_zero_left`, `nthRoot_zero_right`, `pow_nthRoot_le`, `pow_nthRoot_le_iff`	14
Total	15

Nat

Definitions

Name	Category	Theorems
`instDecidableExistsPowEq` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_pow_eq_iff` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid` `nthRoot`	—	`eq_or_ne`
`exists_pow_eq_iff'` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid` `nthRoot`	—	`nthRoot_pow`
`le_nthRoot_iff` 📖	mathematical	—	`nthRoot` `Monoid.toNatPow` `instMonoid`	—	`le_or_gt` `le_trans` `pow_le_pow_left'` `instMulLeftMono` `covariant_swap_mul_of_covariant_mul` `pow_nthRoot_le` `LT.lt.not_ge` `LT.lt.trans_le` `lt_pow_nthRoot_add_one`
`lt_pow_nthRoot_add_one` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid` `nthRoot`	—	`pow_one` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `instZeroLEOneClass` `LT.lt.trans_le`
`nthRoot_eq_of_le_of_lt` 📖	mathematical	`Monoid.toNatPow` `instMonoid`	`nthRoot`	—	`eq_or_ne` `le_nthRoot_iff` `nthRoot_lt_iff`
`nthRoot_lt_iff` 📖	mathematical	—	`nthRoot` `Monoid.toNatPow` `instMonoid`	—	`le_nthRoot_iff`
`nthRoot_one_left` 📖	mathematical	—	`nthRoot`	—	—
`nthRoot_one_right` 📖	mathematical	—	`nthRoot`	—	`one_pow` `instZeroLEOneClass` `mul_one` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `instCanonicallyOrderedAdd` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `instNontrivial` `instAtLeastTwoHAddOfNat`
`nthRoot_pow` 📖	mathematical	—	`nthRoot` `Monoid.toNatPow` `instMonoid`	—	`eq_of_forall_le_iff` `le_nthRoot_iff` `StrictMono.le_iff_le` `pow_left_strictMono`
`nthRoot_zero_left` 📖	mathematical	—	`nthRoot`	—	—
`nthRoot_zero_right` 📖	mathematical	—	`nthRoot`	—	—
`pow_nthRoot_le` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid` `nthRoot`	—	`pow_nthRoot_le_iff`
`pow_nthRoot_le_iff` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid` `nthRoot`	—	`zero_add` `pow_one`

Nat.nthRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lt_pow_go_succ_aux` 📖	mathematical	—	`Monoid.toNatPow` `Nat.instMonoid`	—	`pow_le_pow_left'` `Nat.instMulLeftMono` `covariant_swap_mul_of_covariant_mul` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`

---

← Back to Index