## Stream: Beginner Questions

### Topic: sqrt

#### zibo yang (Apr 22 2021 at 16:31):

Hi, is there any lemma or theorem in HOL library like: "a>=0 --> b>=0 --> sqrt(a * b) =sqrt(a) *sqrt(B)"

#### Mathias Fleury (Apr 22 2021 at 16:33):

Have you tried to search for it?

#### Jakub Kądziołka (Apr 22 2021 at 16:34):

the query `"sqrt (?a * ?b)"` finds the relevant theorem

#### Mathias Fleury (Apr 22 2021 at 16:34):

The standard ways are:

``````find_theorems "sqrt (?a * ?b) = sqrt ?a * sqrt ?b"
``````

or

`````` sledgehammer
(*and looking at the used facts*)
``````

#### zibo yang (Apr 22 2021 at 16:36):

thanks a lot. I get some clues

#### Mathias Fleury (Apr 22 2021 at 16:38):

`````` a>=0 ==> b>=0 ==> sqrt(a * b) =sqrt(a) *sqrt(B)
``````

with meta-implication instead of HOL implications

#### zibo yang (Apr 22 2021 at 16:38):

another stupid question: is "r ^ 2" the right form to type when expressing the square of r

yeah

#### Jakub Kądziołka (Apr 22 2021 at 16:51):

if you want to unfold it into `r * r` later, use `power2_eq_square`

#### zibo yang (Apr 22 2021 at 16:55):

ok.I got it

Last updated: Sep 25 2021 at 08:21 UTC