# Zulip Chat Archive

## Stream: maths

### Topic: type class instance error

#### Ashvni Narayanan (Dec 02 2020 at 16:14):

I am trying to state that, te^{Xt} / (e^t - 1) = \sum_{n=1}^{\infty} B_n(X) * t^n / n!, where B_n(X) are Bernoulli polynomials.

```
import number_theory.bernoulli
import data.nat.basic
import analysis.complex.roots_of_unity
import data.complex.exponential
noncomputable theory
def bernoulli_polynomial (n : ℕ) : ℂ → ℂ := λ X, ∑' i : fin (n+1), (bernoulli n)*(nat.choose n i)*(X^(n-i))
lemma one_sub_eq_neg : ∀ n : ℕ, ∀ X : ℂ, bernoulli_polynomial n (1 - X) = (-1)^n * bernoulli_polynomial n X :=
begin
sorry
end
lemma exp_bernoulli : ∀ t : ℕ, ∀ X : ℕ, ∑' i : ℕ, (bernoulli_polynomial i X) * t^i / (nat.factorial i) = (t * real.exp (X * t))/(real.exp t - 1) :=
begin
sorry
end
```

I get the error

```
failed to synthesize type class instance for
t X : ℕ
⊢ add_comm_monoid Prop
```

I don't see where the `add_comm_monoid`

condition is needed.

Thank you for your help!

#### Reid Barton (Dec 02 2020 at 16:15):

I think you must have the wrong $\Sigma$

#### Ashvni Narayanan (Dec 02 2020 at 16:21):

Putting `∑`

instead of `∑'`

gives me an error :

```
unexpected token
```

#### Reid Barton (Dec 02 2020 at 16:23):

Ah, I think there is some `open_locale`

needed maybe?

#### Reid Barton (Dec 02 2020 at 16:23):

https://leanprover-community.github.io/mathlib_docs/algebra/big_operators/basic.html

#### Yakov Pechersky (Dec 02 2020 at 16:23):

`open_locale big_operators`

?

#### Ashvni Narayanan (Dec 02 2020 at 16:27):

Yakov Pechersky said:

`open_locale big_operators`

?

Adding this gives me an error

```
failed to synthesize type class instance for
t X : ℕ
⊢ fintype ℕ
```

since, I think, `∑`

is for finite sums. Putting `∑'`

gives me the original error.

#### Shing Tak Lam (Dec 02 2020 at 16:30):

I think you're missing some brackets, if you add brackets around the sum it works

```
lemma exp_bernoulli : ∀ t : ℕ, ∀ X : ℕ, (∑' i : ℕ, (bernoulli_polynomial i X) * t^i / (nat.factorial i)) = (t * real.exp (X * t))/(real.exp t - 1) :=
begin
sorry
end
```

it works

#### Ashvni Narayanan (Dec 02 2020 at 16:40):

Shing Tak Lam said:

I think you're missing some brackets, if you add brackets around the sum it works

`lemma exp_bernoulli : ∀ t : ℕ, ∀ X : ℕ, (∑' i : ℕ, (bernoulli_polynomial i X) * t^i / (nat.factorial i)) = (t * real.exp (X * t))/(real.exp t - 1) := begin sorry end`

it works

Yeah, that works. Why are the brackets needed though?

#### Yakov Pechersky (Dec 02 2020 at 16:41):

Because the sum operator is ~~higher~~ different precedence than the `=`

, such that it sums over the whole equality proposition term

#### Ashvni Narayanan (Dec 02 2020 at 17:29):

I see. Thank you!

Last updated: May 19 2021 at 02:10 UTC