Theorems · Theorem · commutative algebra
Nat.cast_pow
∀ {α : Type u_1} [inst : Semiring α] (m n : ℕ), ↑(m ^ n) = ↑m ^ n- Defined in
- Mathlib.Data.Nat.Cast.Basic
- Cited by
- 131 results in Mathlib
- Foundations
- Depth 20 from the axioms, rests on 192 definitions · uses propext
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
Cited by131
Results whose statement or proof uses this declaration.
- map_wittStructureIntproof · cited by 13
- IsSelfAdjoint.spectralRadius_eq_nnnormproof · cited by 7
- Rat.cast_powproof · cited by 7
- padicNorm.dvd_iff_norm_leproof · cited by 5
- IsPGroup.card_modEq_card_fixedPointsproof · cited by 4
- PadicInt.zmod_cast_comp_toZModPowproof · cited by 4
- IsCyclotomicExtension.discr_prime_pow_ne_twoproof · cited by 4
- hasSum_choose_mul_geometric_of_norm_lt_one'proof · cited by 4
- Cardinal.power_lt_aleph0proof · cited by 4
- PadicInt.appr_specproof · cited by 4
- Pell.exists_of_not_isSquareproof · cited by 3
- NumberField.HeightOneSpectrum.embedding_mul_absNormproof · cited by 3