## Stream: new members

### Topic: Integral of real.sqrt

#### James Arthur (Jan 08 2021 at 11:35):

Hi,
I'm trying to prove the area of a circle and so I need to do the integral of a sqrt, this is th current setup,

import data.real.basic analysis.special_functions.trigonometric
import measure_theory.interval_integral
import data.real.sqrt

example (r : ℝ) (x : ℝ) : ∫ (real.sqrt x) in 0..r, x = r :=
begin
sorry
end


and it gives me an error I don't understnad, it gives,

invalid binder, atomic identifier expected


What does this mean / how can I fix it?

#### Kenny Lau (Jan 08 2021 at 11:37):

I think you need to open_locale something

#### Shing Tak Lam (Jan 08 2021 at 11:47):

Also isn't the syntax ∫ x in (0 : ℝ) .. r, real.sqrt x?

#### James Arthur (Jan 08 2021 at 11:49):

Ooooh, is it? I went from the integral of x example where it gets confusing and assumed it was like deriv

#### James Arthur (Jan 08 2021 at 11:50):

IT WORKS, IT WAS JUST ME BEING STUPID!

#### Kevin Buzzard (Jan 08 2021 at 11:50):

lucky Zulip doesn't have that capital letter warning bot like the discord ;-)

#### James Arthur (Jan 08 2021 at 11:51):

haha, indeed. I can use all the caps I want!

#### Răzvan Flavius Panda (Jan 08 2021 at 11:52):

oh, now I WANT TO TRY THAT to see what the bot does

image.png

#### Kevin Buzzard (Jan 08 2021 at 11:52):

I think we can save the spam for the discord

Last updated: May 14 2021 at 00:42 UTC