Theorem Nat.mul_le_pow

Modification history

2026-05-18 09:40
Mathlib/Data/Nat/Basic.lean
chore(Data/Nat/Cast/Order/Ring): move two Nat lemmas to Data/Nat/Basic (#38343) …
Modified Nat.mul_le_powView on Github →
2024-08-04 14:32
Mathlib/Data/Nat/Cast/Order/Ring.lean
feat: Real.exists_natCast_add_one_le_pow_of_one_le (#15074) …
Added Nat.mul_le_powView on Github →