Does anyone know where a lemma similar to
∃(x::real). a^x = (b::real)
might be found? I couldn't find something like that in the 'query', but it seems pretty handy.
Does anyone know where a lemma similar to
∃(x::real). a^x = (b::real)
might be found? I couldn't find something like that in the 'query', but it seems pretty handy.
You need a few more assumptions on
a
andb
and you need to use thepowr
operator instead of^
, since^
is only for then
-th power wheren
is a natural number.powr
on the other hand is for any non-negative real number raised to the power of any other real number. (or similarly for complex numbers)