## Stream: maths

### Topic: Definition of nat multiplication

#### Sebastien Gouezel (Jan 05 2021 at 20:56):

I posted a question on the lean4 thread asking if the Lean4 developers would agree to change the definition of nat multiplication to avoid non-defeq instances of semimodule on nat. Leo's answer was very reasonable: they may consider this, but first all users should agree on this. https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/PR.20welcome.3F/near/221693092

I have the impression that this change would solve a problem we have encountered in Lean 3, but if I understand correctly @Eric Wieser was not convinced it would really solve the issue. Since I'm not completely sure either way, I thought I'd ask here. What do you think?

#### Johan Commelin (Jan 05 2021 at 20:58):

I think it will at least solve more problems than it will create (from a maths perspective). I have no idea if there are CS reasons to keep it the way it is.

#### Eric Wieser (Jan 05 2021 at 21:21):

Did you mean to link to the same topic you posted in?

#### Gabriel Ebner (Jan 05 2021 at 21:29):

I'm not sure there's a reason for the right-recursiveness of multiplication except to be consistent with addition. (And I really prefer n+1 over 1+n.)

#### Gabriel Ebner (Jan 05 2021 at 21:30):

If we want to change this in Lean 4, we should first try it out in Lean 3 and see if there's any unexpected breakage in mathlib.

#### Floris van Doorn (Jan 05 2021 at 22:30):

So is the suggestion to keep addition right-recursive? I agree with Gabriel that n+1 looks much nicer than 1+n.
Left-recursive multiplication and right-recursive addition sounds weird, but maybe that's pretty nice. 2 * n looks nicer than (or equally nice as) n * 2.

#### Eric Wieser (Jan 06 2021 at 14:54):

Ok, here's the diamond in nat.semimodule that this won't help with removing:

import algebra.module.basic

@[ext]
structure has_nat_diamond (M : Type*) :=
(value : M)

namespace has_nat_diamond

variables {M : Type*}

{ zero := ⟨0⟩,
add := λ a b, ⟨a.1 + b.1⟩,
add_assoc := λ a b c, ext _ _ (add_assoc _ _ _) }

instance {R : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] :
semimodule R (has_nat_diamond M) :=
{ smul := λ r x, ⟨r • x.1⟩,
one_smul := λ _, ext _ _ (one_smul _ _),
mul_smul := λ _ _ _, ext _ _ (mul_smul _ _ _),
smul_add := λ _ _ _, ext _ _ (smul_add _ _ _),
smul_zero := λ _, ext _ _ (smul_zero _),
add_smul := λ _ _ _, ext _ _ (add_smul _ _ _),
zero_smul := λ _, ext _ _ (zero_smul _ _) }

-- fails
example {R : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] :
(add_comm_monoid.nat_semimodule : semimodule ℕ (has_nat_diamond M)) = has_nat_diamond.semimodule := rfl

end has_nat_diamond


#### Eric Wieser (Jan 06 2021 at 14:57):

The proof := subsingleton.elim _ _ works, but type-class resolution doesn't try that

#### Eric Wieser (Jan 06 2021 at 14:58):

That's not to say that your suggestion is pointless - it does solve diamonds between docs#mul_action.regular and docs#add_comm_monoid.nat_semimodule

#### Sebastien Gouezel (Jan 06 2021 at 16:05):

Yes indeed, the diamond you're pointing out is not solved by my proposition, which is only to solve the two ℕ-modules structure on ℕ.

#### Eric Wieser (Jan 06 2021 at 16:14):

The diamond above is quite pervasive - because it affects linear_map, a chain of N linear maps has N+1 different nat-semimodule instances

#### Sebastien Gouezel (Jan 08 2021 at 12:48):

Gabriel Ebner said:

If we want to change this in Lean 4, we should first try it out in Lean 3 and see if there's any unexpected breakage in mathlib.

I had a look at the change in Lean 3, and there is an issue that there is non-homogeneous multiplication in Lean 4 but not in Lean 3, so making the "same" change and checking the consequences does not seem obvious. In Lean 4, it would be possible to define a multiplication ℕ → α → α for any α with an addition and a zero, by induction, and then specialize it to a multiplication on ℕ. And then define a multiplication ℤ → α → α  for any α with an addition, a zero and a negation (by using the nat addition already defined), and specialize it to get the ℤ-multiplication. In the current state of Lean 3 and mathlib, making the same change would require moving has_scalar to core, so I am not sure it is desirable.

#### Eric Wieser (Jan 08 2021 at 12:50):

For what it's worth, there's now a docs#nsmul_eq_smul lemma that will rewrite the "backwards" multiplication of docs#add_comm_monoid.int_semimodule into the forwards multiplication of docs#mul_action.regular, as long as you use local attribute [instance] mul_action.regular

Last updated: May 11 2021 at 17:39 UTC