# Zulip Chat Archive

## 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*}
instance [add_comm_monoid M] : add_comm_monoid (has_nat_diamond M) :=
{ zero := ⟨0⟩,
add := λ a b, ⟨a.1 + b.1⟩,
zero_add := λ a, ext _ _ (zero_add _),
add_zero := λ a, ext _ _ (add_zero _),
add_comm := λ a b, ext _ _ (add_comm _ _),
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