## 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