Theorems · Theorem · number theory
Rat.cast_pow
∀ {α : Type u_1} [inst : DivisionRing α] (p : ℚ) (n : ℕ), ↑(p ^ n) = ↑p ^ n- Defined in
- Mathlib.Data.Rat.Cast.Lemmas
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 54 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DivisionRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DivisionRingstatement and proof · cited by 1,062
- div_eq_mul_invproof · cited by 715
- inv_powproof · cited by 140
- Nat.cast_powproof · cited by 131
- Int.cast_powproof · cited by 59
- Commute.mul_powproof · cited by 22
- Rat.cast_defproof · cited by 20
- Int.cast_commuteproof · cited by 7
Cited by7
Results whose statement or proof uses this declaration.
- irrational_nrt_of_notint_nrtproof · cited by 2
- Finpartition.coe_energyproof · cited by 1
- Real.infinite_rat_abs_sub_lt_one_div_den_sq_iff_irrationalproof · cited by 0
- Nat.realSqrt_lt_ratSqrt_add_inv_precproof · cited by 0
- riemannZeta_neg_nat_eq_bernoulliproof · cited by 0
- padicNorm_two_harmonicproof · cited by 0