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