Mathlib Map

Theorems · Theorem · number theory

ENat.epow_natCast

∀ {x : ℕ∞} {y : ℕ}, x ^ ↑y = x ^ y
Defined in
Mathlib.Data.ENat.Pow
Cited by
5 results in Mathlib
Foundations
Depth 33 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.

ENat.one_epow · cited by 7ENat.one_epowENat.epow_zero · cited by 6ENat.epow_zeroENat.zero_epow · cited by 4ENat.zero_epowENat.epow_one · cited by 2ENat.epow_oneENat.top_epow · cited by 2ENat.top_epowENat · cited by 4985ENatENat.epow_natCastCITED BYCITES

Cites1

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

  • ENatstatement and proof · cited by 4,985

Cited by5

Results whose statement or proof uses this declaration.