Pow

📁 Source: Mathlib/Data/Nat/Prime/Pow.lean

Statistics

Metric	Count
Definitions	0
Theorems pow_minFac, pow_minFac	2
Total	2

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pow_minFac 📖	mathematical	—	minFac Monoid.toNatPow instMonoid	—	eq_or_ne one_pow minFac_one pow_eq_one_iff_left instIsMulTorsionFree LE.le.antisymm minFac_le_of_dvd Prime.two_le minFac_prime Dvd.dvd.pow minFac_dvd Prime.dvd_of_dvd_pow

Nat.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pow_minFac 📖	mathematical	Nat.Prime	Nat.minFac Monoid.toNatPow Nat.instMonoid	—	Nat.pow_minFac minFac_eq

---

← Back to Index