Hi, is there any lemma or theorem in HOL library like: "a>=0 --> b>=0 --> sqrt(a * b) =sqrt(a) *sqrt(B)"
Have you tried to search for it?
"sqrt (?a * ?b)" finds the relevant theorem
The standard ways are:
find_theorems "sqrt (?a * ?b) = sqrt ?a * sqrt ?b"
sledgehammer (*and looking at the used facts*)
thanks a lot. I get some clues
BTW, your lemma should be
a>=0 ==> b>=0 ==> sqrt(a * b) =sqrt(a) *sqrt(B)
with meta-implication instead of HOL implications
another stupid question: is "r ^ 2" the right form to type when expressing the square of r
if you want to unfold it into
r * r later, use
ok.I got it
Last updated: Sep 25 2021 at 08:21 UTC