nat.pow_pos

Stream: Is there code for X?

[Ruben Van de Velde]

Is there a reason to have both of these?

theorem nat.pos_pow_of_pos {b : ℕ} (n : ℕ) : 0 < b → 0 < b ^ n
theorem nat.pow_pos {p : ℕ} (hp : 0 < p) (n : ℕ) : 0 < p ^ n

and do we not have

lemma nat.pos_pow_iff {b : ℕ} (n : ℕ) (h : 0 < n) : 0 < b ↔ 0 < b ^ n

at all?

[Johan Commelin]

Just historical accidents... Note that it is likely better to swap the sides of the pos_pow_iff statement.
Feel free to PR.

[Rob Lewis]

0^0 = 1, no?

[Ruben Van de Velde]

Hence the 0 < n hypothesis, yeah

[Rob Lewis]

Oh, duh.