# Zulip Chat Archive

## Stream: new members

### Topic: Question about namespace

#### Alfredo (Feb 03 2022 at 17:41):

Hi all, i am very new to lean so trying to do some easy cleanup task, however as a begginier, i have some problems that i can't figure out. I made a draft PR to ask a question: https://github.com/leanprover-community/mathlib/pull/11805

Any input will be great, thanks in advance.

#### Eric Rodriguez (Feb 03 2022 at 17:44):

hiya Alfredo, you should try move this to another thread!

#### Riccardo Brasca (Feb 03 2022 at 17:45):

I've moved the message to a new thread.

#### Riccardo Brasca (Feb 03 2022 at 17:46):

(feel free to modify the title)

#### Alfredo (Feb 03 2022 at 17:53):

ops, sorry about that. thanks for the move, title looks good.

#### Riccardo Brasca (Feb 04 2022 at 07:44):

What is the error you are getting?

#### Alfredo (Feb 04 2022 at 12:10):

forgot to post that:

```
type mismatch at application
has_mul.mul X
term
X
has type
polynomial ?m_1 : Type ?
but is expected to have type
power_series A : Type u_1
```

#### Johan Commelin (Feb 04 2022 at 13:01):

It looks like lean thinks you are trying to multiply polynomials whereas it expects you to multiply power series.

#### Johan Commelin (Feb 04 2022 at 13:01):

Does writing `power_series.X`

instead of `X`

help?

#### Alfredo (Feb 04 2022 at 13:13):

i think i tried, the error change to a lower line if we do that

#### Alfredo (Feb 04 2022 at 13:14):

it will fial in the `rw`

line:

```
rw [coeff_succ_X_mul, coeff_rescale, coeff_exp, coeff_mul,
nat.sum_antidiagonal_eq_sum_range_succ_mk, sum_range_succ],
```

with error:

```
error: rewrite tactic failed, did not find instance of the pattern in the target expression
(?m_3 * ?m_4).coeff ?m_5
state:
A : Type u_1,
_inst_1 : comm_ring A,
_inst_2 : algebra ℚ A,
t : A,
n : ℕ
⊢ ⇑(power_series.coeff A n.succ)
(mk (λ (n : ℕ), ⇑(aeval t) ((1 / ↑n!) • bernoulli_poly n)) * (exp A - 1)) =
t ^ n * ⇑(algebra_map ℚ A) (1 / ↑n!)
external command exited with status 1
```

#### Johan Commelin (Feb 04 2022 at 13:16):

Did you move things from the `power_series`

namespace to a place working inside the `polynomial`

namespace?

#### Alfredo (Feb 04 2022 at 13:18):

i dont think i did that

can you explain more ?

#### Riccardo Brasca (Feb 04 2022 at 13:19):

I suggested to work in the `polynomial`

namespace (since the file is about Bernoulli polynomials). Let me check what's going on.

#### Alfredo (Feb 04 2022 at 13:20):

yea, that is what i am trying to do, i can add everything to the polynomial namespace without issues but the second theorem is the one that fails when we do that

#### Riccardo Brasca (Feb 04 2022 at 13:26):

Here is what is going on: writing `namespace polynomial`

means that all the lemma will have `polynomial`

in the name, so for example `lemma foo`

will be called `polynomial.foo`

(this answer your first comment about collision with another name).

#### Riccardo Brasca (Feb 04 2022 at 13:27):

It also means that if a lemma is called `polynomial.bar`

you can use it just writing `bar`

(so `namespace polynomial`

implies `open polynomial`

, and this line can be deleted).

#### Riccardo Brasca (Feb 04 2022 at 13:27):

In the file there is also `open power_series`

, to avoid writing `power_series.exp`

and similar stuff.

#### Alfredo (Feb 04 2022 at 13:27):

yes

#### Riccardo Brasca (Feb 04 2022 at 13:28):

Now, there is `polynomial.X`

and `power_series.X`

in mathlib, and this confuses Lean, since now both are called `X`

. This is why you got the first error: Lean tried to use `polynomial.X`

, but there one should use `power_series.X`

. You can help it writing `power_series.X`

in that location.

#### Alfredo (Feb 04 2022 at 13:30):

right

#### Riccardo Brasca (Feb 04 2022 at 13:30):

The second error is similar: it says

```
rewrite tactic failed, did not find instance of the pattern in the target expression
(?m_3 * ?m_4).coeff ?m_5
```

In the line

```
rw [coeff_succ_X_mul, coeff_rescale, coeff_exp, coeff_mul,
nat.sum_antidiagonal_eq_sum_range_succ_mk, sum_range_succ],
```

Looking at the error one can guess that it's something related to `coeff_mul`

(you can also delete one lemma after the other to see which one creates problems).

#### Riccardo Brasca (Feb 04 2022 at 13:31):

And indeed we have both `polynomial.coeff_mul`

and `power_series.coeff_mul`

.

#### Riccardo Brasca (Feb 04 2022 at 13:31):

Here again the correct one is the latter, so with `power_series.coeff_mul`

the error goes away.

#### Alfredo (Feb 04 2022 at 13:33):

cool, you are the best, thank you!

#### Alfredo (Feb 04 2022 at 13:34):

i made an additional comment about the first question

#### Riccardo Brasca (Feb 04 2022 at 13:35):

The same error occurs again later, but it's a little trickier to understand: it says that it cannot use `apply congr_arg`

to make progress, but this is because the previous line, the one with `simp only`

changed it's effect and it has become less efficient. You should replace `coeff_one`

with `power_series.coeff_one`

and then everything works.

#### Alfredo (Feb 04 2022 at 13:35):

awsome

#### Riccardo Brasca (Feb 04 2022 at 13:36):

Concerning your new comment: I don't understand what you mean, I don't have any error.

#### Riccardo Brasca (Feb 04 2022 at 13:37):

Can I push a commit to your branch?

#### Alfredo (Feb 04 2022 at 13:37):

sure

#### Riccardo Brasca (Feb 04 2022 at 13:39):

Ah sorry, now I got what you mean. Yes, if you want to use `bernoulli`

you can write `_root_.bernoulli`

.

#### Riccardo Brasca (Feb 04 2022 at 13:40):

```
/-- The Bernoulli polynomials are defined in terms of the negative Bernoulli numbers. -/
def bernoulli (n : ℕ) : polynomial ℚ :=
∑ i in range (n + 1), polynomial.monomial (n - i) ((bernoulli i) * (choose n i))
lemma bernoulli_def (n : ℕ) : bernoulli n =
∑ i in range (n + 1), polynomial.monomial i ((_root_.bernoulli (n - i)) * (choose n i)) :=
begin
rw [←sum_range_reflect, add_succ_sub_one, add_zero, bernoulli],
apply sum_congr rfl,
rintros x hx,
rw mem_range_succ_iff at hx, rw [choose_symm hx, tsub_tsub_cancel_of_le hx],
end
```

This works. (There are other changes to be done later in the file.)

#### Alfredo (Feb 04 2022 at 13:57):

apologies, had to go out for a bit

#### Alfredo (Feb 04 2022 at 13:59):

thank you for the help , i will try to do the other changes suggested, i think there are just lemma name changes left

Last updated: Dec 20 2023 at 11:08 UTC