# Zulip Chat Archive

## Stream: new members

### Topic: semigroup.to_has_mul versus nat.has_mul

#### Moritz Firsching (Feb 17 2021 at 20:50):

Consider the following proof attempt to a simple lemma:

```
import tactic
lemma factorial_divide (n m : ℕ) (hmn: m ≤ n):
((m.factorial * (n-m).factorial)) ∣ (n.factorial) :=
begin
have chosse_mul:
(n.choose m)* ((m.factorial * (n-m).factorial)) = (n.factorial) :=
begin
simp [nat.choose_eq_factorial_div_factorial hmn],
-- simp [div_mul_eq_mul_div], why doesn't this work?
sorry,
end,
apply dvd.intro_left ((n.choose m)),
-- exact choose_mul, why doesn't this work?
sorry,
end
```

I'm a bit stumped that e.g. in the after the line `apply dvd.intro_left ((n.choose m)),`

I see the exact same state in the goal and in choose_mul in the lean infoview. When I click on the terms, I can see there is some difference, but how can I actually get control over how the division/multiplication is done when defining `choose_mul`

?

#### Kevin Buzzard (Feb 17 2021 at 20:52):

The second question is easy to answer -- you made a typo :-) `chosse`

-> `choose`

#### Moritz Firsching (Feb 17 2021 at 20:54):

cool, that explains solves the second "why doesn't this work?"!

#### Kevin Buzzard (Feb 17 2021 at 20:54):

As for the first, `#check @div_mul_eq_mul_div`

shows you that it's a theorem which applies to `comm_group_with_zero`

s, and the naturals are not an example of a `comm_group_with_zero`

.

#### Kevin Buzzard (Feb 17 2021 at 20:56):

In fact there will not be a theorem of the form `(a / b) * b = a`

for naturals, because this is not true in general, e.g. `(3 / 2) * 2 = 1 * 2 = 2`

:-/

#### Kevin Buzzard (Feb 17 2021 at 20:56):

to prove `a / b * b = a`

for nats you need the assumption that b divides a, which unfortunately is what you're trying to prove :-/

#### Kevin Buzzard (Feb 17 2021 at 20:58):

The result you're trying to prove is already in the library -- it's called `nat.factorial_mul_factorial_dvd_factorial`

, so you can prove it with `by library_search`

. But if you're looking for a proof of your own then maybe this doesn't help.

#### Kevin Buzzard (Feb 17 2021 at 21:00):

There is also `nat.choose_mul_factorial_mul_factorial`

#### Moritz Firsching (Feb 17 2021 at 21:01):

Thanks I will just check out how those proofs work! (and meanwhile just use them)

Last updated: May 17 2021 at 22:15 UTC