Division by 1

Stream: new members

[Bob Rubbens]

Can someone point me in the right direction? Likely I just haven't read enough docs but I can't find the page explaining how to do this:

def div_one : m / 1 = m := by
  sorry

[Eric Rodriguez]

what is m?

[Damiano Testa]

Also, probably theorem or example, rather than def.

[Bob Rubbens]

Ah, I would like it to be a number, but if it makes things easier assume it is a Nat!

[Bob Rubbens]

I just noticed there is also div_eq, so probably I can force push my way through this, but if there is an elegant way of doing it I would love to hear so

[Damiano Testa]

In std this lemma already exists: docs#Nat.div_one`. Is this what you are looking for?

[Bob Rubbens]

Yes! I guess I don't have matlib4 installed because simp doesn't close the goal for me...?

[Damiano Testa]

You do not even have Std, it seems.

[Eric Rodriguez]

At some point you will have to prove something by induction, that's just the way it is. What do you mean by "number"? Real, rational?

[Eric Rodriguez]

This can be proved for docs#DivInvMonoid s, I think, but it's somewhat cheating...

e: docs#DivInvOneMonoid !

[Bob Rubbens]

I guess I just want to prove it for Nat, then, I'm not looking to prove it for anything else.

[Bob Rubbens]

Damiano Testa said:

You do not even have Std, it seems.

If I do "#check Std" indeed I can't ctrl+click to anything. Is this part of matlib or a more general package?

[Damiano Testa]

Rather than #check, try import Std. Mathlib depends on Std, so, in some sense, it is Std that is a part of Mathlib, not the other way round.

[Damiano Testa]

If you intend to do anything at all mathematical, almost certainly it will be beneficial to use Mathlib. Not depending on Std means really going way back!

[Bob Rubbens]

This answers many more questions than I intended to ask. Thanks!