Mathlib Map

Theorems · Theorem · number theory

NNRat.den_pow

∀ (q : ℚ≥0) (n : ℕ), (q ^ n).den = q.den ^ n
Defined in
Mathlib.Data.NNRat.Defs
Cited by
1 results in Mathlib
Foundations
Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

NNRat.cast_pow · cited by 1NNRat.cast_powNNRat · cited by 523NNRatNNRat.den · cited by 51NNRat.denNNRat.den_powCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • NNRatstatement and proof · cited by 523
  • NNRat.denstatement · cited by 51

Cited by1

Results whose statement or proof uses this declaration.