Theorems · Theorem · complex analysis
Complex.pow_cpow_nat_inv
∀ {x : ℂ} {n : ℕ}, n ≠ 0 → -(Real.pi / ↑n) < x.arg → x.arg ≤ Real.pi / ↑n → (x ^ n) ^ (↑n)⁻¹ = x- Cited by
- 1 results in Mathlib
- Foundations
- Depth 198 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Complexstatement and proof · cited by 5,565
- Real.pistatement and proof · cited by 1,774
- Complex.argstatement and proof · cited by 220
- mul_inv_cancel₀proof · cited by 210
- neg_divproof · cited by 161
- Ne.bot_ltproof · cited by 116
- Nat.cast_ne_zeroproof · cited by 113
- Nat.cast_posproof · cited by 113
- le_div_iff₀'proof · cited by 32
- Complex.cpow_oneproof · cited by 20
- div_lt_iff₀'proof · cited by 20
Cited by1
Results whose statement or proof uses this declaration.
- Complex.pow_cpow_ofNat_invproof · cited by 1