# Zulip Chat Archive

## Stream: maths

### Topic: smul_eq_mul

#### Ashvni Narayanan (Feb 16 2021 at 11:49):

I have the following definition :

```
import number_theory.bernoulli
def bernoulli_neg (n : ℕ) : ℚ := (-1)^n * (bernoulli n)
```

I am trying to show

```
bernoulli_neg n • 1 + ∑ (x : ℕ) in range n, (bernoulli_neg x * ↑(n.choose x)) • 0 ^ (n - x) = bernoulli_neg n
```

`algebra.id.smul_eq_mul`

and `mul_one`

don't seem to help with `bernoulli_neg n • 1`

, where `1 : ℚ`

. I don't understand why, because it works if I put it as a separate lemma.

Any help is appreciated, thank you!

#### Eric Wieser (Feb 16 2021 at 12:03):

How are you using the lemma?

#### Eric Wieser (Feb 16 2021 at 12:03):

Can you give a #mwe demonstrating the failure?

#### Ashvni Narayanan (Feb 16 2021 at 13:23):

Apologies for the late reply. I found an alternate solution to my problem. However, I find it very strange that if I make a lemma of the above statement, then I can solve it using `algebra.id.smul_eq_mul`

, but it does not seem to work in the theorem I am trying to prove :

```
import number_theory.bernoulli
noncomputable theory
open_locale big_operators
open finset
def bernoulli_neg (n : ℕ) : ℚ := (-1)^n * (bernoulli n)
variables {A : Type*} [comm_semiring A] [algebra ℚ A]
def bernoulli_poly (n : ℕ) : A → A := λ X, ∑ i in finset.range (n+1),
((bernoulli_neg i)*(nat.choose n i)) • (X^(n-i))
@[simp] lemma bernoulli_poly_zero' (n : ℕ) : bernoulli_poly n 0 = bernoulli_neg n :=
begin
rw bernoulli_poly, dsimp only,
suffices : ∑ (x : ℕ) in range n, (bernoulli_neg x * (n.choose x)) * 0 ^ (n - x) = 0,
{ rw sum_range_succ, simp, rw ←algebra.algebra_map_eq_smul_one, simp only [add_right_eq_self,
ring_hom.id_apply, rat.algebra_map_rat_rat], apply sum_eq_zero, rintros x Hx,
rw zero_pow',
{ sorry,},
{ intros h, apply nat.lt_le_antisymm (mem_range.1 Hx) (nat.sub_eq_zero_iff_le.1 h), },
},
sorry,
end
```

Originally, I wanted to use `smul_eq_mul`

after the `simp`

on the line after `suffices`

. However, I seem to be having the same issue with using `smul_zero`

on the first `sorry`

line.

#### Kevin Buzzard (Feb 16 2021 at 13:34):

`convert smul_zero _`

solves the first `sorry`

. You don't seem to be doing anything weird with typeclasses here, I don't know why `exact smul_zero _`

doesn't work, but you're right, it doesn't.

#### Kevin Buzzard (Feb 16 2021 at 13:36):

There is just some stupid typeclass issue with `has_scalar.smul`

.

#### Ashvni Narayanan (Feb 16 2021 at 13:38):

Is there something I can do about it? I have a feeling I am going to be encountering this problem a lot more going ahead.

#### Kevin Buzzard (Feb 16 2021 at 13:38):

Your problem is that you are using smul at all, rather than using `polynomial ℚ`

. Every polynomial with rational coefficients gives you a map A -> A for any Q-algebra A, but you don't want to encode a polynomial as a collection of functions, you want to encode it as a polynomial.

#### Kevin Buzzard (Feb 16 2021 at 13:39):

You should make the polynomial as a term of type `polynomial Q`

and then there are various `eval`

functions you can use to create the functions from A to A.

#### Eric Wieser (Feb 16 2021 at 13:52):

There's definitely a problem hiding here

#### Ashvni Narayanan (Feb 16 2021 at 13:52):

Kevin Buzzard said:

You should make the polynomial as a term of type

`polynomial Q`

and then there are various`eval`

functions you can use to create the functions from A to A.

I see, that makes sense, thank you!

#### Eric Wieser (Feb 16 2021 at 13:53):

I was able to get lean to spit out what I assume is causing the unification issue when trying to apply `mul_eq_smul`

```
@algebra.to_semimodule ℚ ℚ rat.comm_semiring (@comm_semiring.to_semiring ℚ rat.comm_semiring)
(@rat.algebra_rat ℚ rat.division_ring _) =
@semiring.to_semimodule ℚ rat.semiring
```

by adding this at the first sorry:

```
suffices : (bernoulli_neg x * ↑(n.choose x)) * 0 = 0,
{ rw ←smul_eq_mul at this,
convert this,
sorry},
```

#### Eric Wieser (Feb 16 2021 at 13:55):

Are we missing a `subsingleton (semimodule ℚ A)`

instance to follow the trend set by docs#add_comm_monoid.nat_semimodule.subsingleton? Or is that statement not true?

#### Ashvni Narayanan (Feb 16 2021 at 13:58):

Eric Wieser said:

I was able to get lean to spit out what I assume is causing the unification issue when trying to apply

`mul_eq_smul`

`@algebra.to_semimodule ℚ ℚ rat.comm_semiring (@comm_semiring.to_semiring ℚ rat.comm_semiring) (@rat.algebra_rat ℚ rat.division_ring _) = @semiring.to_semimodule ℚ rat.semiring`

by adding this at the first sorry:

`suffices : (bernoulli_neg x * ↑(n.choose x)) * 0 = 0, { rw ←smul_eq_mul at this, convert this, sorry},`

Ooh nice, thank you!

#### Kevin Buzzard (Feb 16 2021 at 14:01):

I think there is a subsingleton instance, which is why `convert`

works.

#### Eric Wieser (Feb 16 2021 at 14:01):

The `smul_zero`

problem is a different one

#### Eric Wieser (Feb 16 2021 at 14:05):

`convert smul_zero _ using 2,`

gives you a preview of what's maybe going wrong

#### Eric Wieser (Feb 16 2021 at 14:05):

Although interesting you can get stuck if you use `convert rfl`

after that

#### Eric Wieser (Feb 16 2021 at 14:08):

The closest subsingleton I can think of is docs#rat.algebra_rat_subsingleton, but that's not an instance because we're now scared of adding new subsingleton instances. Making it an instance doesn't help here anyway.

#### Eric Wieser (Feb 16 2021 at 14:14):

This is the statement that is either false or missing:

```
example {A : Type*} [division_ring A] [char_zero A] : subsingleton (semimodule ℚ A) :=
⟨λ x y, semimodule_ext _ _ $ λ q m, begin
sorry,
end⟩
```

#### Kevin Buzzard (Feb 16 2021 at 14:14):

It's true.

#### Kevin Buzzard (Feb 16 2021 at 14:16):

If q=n/d then q.a is the unique solution to d(q.a)=na, and there's a unique Z-module structure on any abelian group.

#### Eric Wieser (Feb 16 2021 at 14:18):

and there's a unique Z-module structure on any abelian group

Thankfully this part exists already as docs#add_comm_group.int_semimodule.subsingleton

#### Kevin Buzzard (Feb 16 2021 at 14:20):

The semimodule instance is a subsingleton for any add_comm_monoid A by the way

#### Eric Wieser (Feb 16 2021 at 14:21):

Ah, I just added `[division_ring A] [char_zero A] `

because the instance doesn't exist at all without those

#### Kevin Buzzard (Feb 16 2021 at 14:21):

Right -- with those it's `unique`

.

#### Kevin Buzzard (Feb 16 2021 at 14:23):

If R is a commutative semiring and L is a localisation of R (e.g. its semifield of fractions) then there's an injection from the L-semimodule structures on M to the R-semimodule structures on N.

#### Kevin Buzzard (Feb 16 2021 at 14:24):

and the image is the R-semimodule structures on N for which all the elements you're localising at act as bijections.

#### Kevin Buzzard (Feb 16 2021 at 14:25):

I think there might already be an instance from `division_ring R`

+ `char_zero R`

to `algebra \Q R`

#### Eric Wieser (Feb 16 2021 at 14:25):

Yes, there is

#### Eric Wieser (Feb 16 2021 at 14:26):

And a proof it's a subsingleton, I link it above

#### Kevin Buzzard (Feb 16 2021 at 14:26):

I see, but asking that the module structure is a subsingleton is a stronger statement.

#### Eric Wieser (Feb 16 2021 at 14:29):

Indeed

#### Eric Wieser (Feb 16 2021 at 14:32):

I can get to:

```
example {A : Type*} [division_ring A] [char_zero A] : subsingleton (semimodule ℚ A) :=
⟨λ x y, semimodule_ext _ _ $ begin
rw rat.forall,
intros a b m,
simp_rw div_eq_mul_inv,
rw x.mul_smul,
rw y.mul_smul,
rw ←@gsmul_eq_smul_cast ℚ _ _ _ x a _,
rw ←@gsmul_eq_smul_cast ℚ _ _ _ y a _,
congr' 1,
sorry,
end⟩
```

at which point I think I need to apply char_zero to `gsmul`

both sides by `b`

#### Eric Wieser (Feb 16 2021 at 14:39):

Solved!

```
example {A : Type*} [ring A] : subsingleton (semimodule ℚ A) :=
⟨λ x y, semimodule_ext _ _ $ begin
rw rat.forall,
intros a b m,
simp_rw div_eq_mul_inv,
rw x.mul_smul,
rw y.mul_smul,
rw ←@gsmul_eq_smul_cast ℚ _ _ _ x a _,
rw ←@gsmul_eq_smul_cast ℚ _ _ _ y a _,
congr' 1,
by_cases hb : (b : ℚ) = 0,
{ rw hb,
simp [x.zero_smul, y.zero_smul], },
rw @inv_smul_eq_iff' _ _ _ x.to_distrib_mul_action.to_mul_action _ hb,
rw ←@gsmul_eq_smul_cast ℚ _ _ _ x b _,
rw @gsmul_eq_smul_cast ℚ _ _ _ y b _,
rw @smul_smul _ _ _ y.to_distrib_mul_action.to_mul_action,
simp [y.one_smul, mul_inv_cancel hb],
end⟩
```

#### Eric Wieser (Feb 16 2021 at 14:39):

I'll leave someone else to golf away the `@`

s...

#### Eric Wieser (Feb 16 2021 at 14:41):

We probably need the full set of `gsmul_eq_smul_cast`

lemmas for a hypothetical `qsmul`

to make the original problem easy to work with though

Last updated: May 12 2021 at 08:14 UTC