scilib documentation

LeanChemicalTheories / math.rpow

source
theorem rpow_ne_zero {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
x ^ y ≠ 0
source
theorem zero_lt_rpow {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
0 < x ^ y