## Stream: general

### Topic: Eckmann–Hilton

#### Johan Commelin (Sep 07 2018 at 08:07):

Today I thought it was a good idea to stretch the type class system a bit. In fact, I ended up not using it at all :rolling_on_the_floor_laughing:
https://gist.github.com/jcommelin/2e031b5446ca54089576ea9f66f12abf
Statement: Two unital binary operations that distribute over each other are in fact one and the same. Also, they are commutative and associative, so in fact a monoid structure.
This is used to prove that homotopy groups are abelian.

#### Johan Commelin (Sep 07 2018 at 08:08):

In particular, feel free to shoehorn this into the type class system.
Golfing is appreciated.

#### Reid Barton (Sep 07 2018 at 08:13):

Nope I hadn't gotten that far. Cool!

#### Reid Barton (Sep 07 2018 at 08:15):

local notation a  m  b := @has_mul.mul X m a b


Does this really work? Also, it doesn't work for me. :)

#### Reid Barton (Sep 07 2018 at 08:17):

Oh nice. Copy and paste from github (even the raw page) doesn't preserve the source text correctly.

#### Reid Barton (Sep 07 2018 at 08:18):

Maybe you could choose something less sneaky like local notation a <m> b := @has_mul.mul X m a b

#### Johan Commelin (Sep 07 2018 at 08:21):

Hmm, maybe I should.

#### Johan Commelin (Sep 07 2018 at 08:21):

But those are non-breaking spaces.

#### Johan Commelin (Sep 07 2018 at 08:24):

Hmmm... that's really nasty of GitHub.

#### Johan Commelin (Sep 07 2018 at 08:24):

They should know better.

#### Johan Commelin (Sep 07 2018 at 08:24):

I'll use fishhooks, like you suggested.

#### Reid Barton (Sep 07 2018 at 08:24):

Somehow when I pasted the source into emacs, they turned into regular spaces.
Not sure whether github or firefox or emacs is to blame

Ok, fair enough.

#### Johan Commelin (Sep 07 2018 at 08:26):

Anyway, it is fixed now.

#### Reid Barton (Sep 07 2018 at 08:35):

Haha, Lean prints both mul operations as *. It knows!!

#### Johan Commelin (Sep 07 2018 at 08:38):

Yes! I thought that was hilarious :rolling_on_the_floor_laughing:

#### Johan Commelin (Sep 07 2018 at 10:16):

@Mario Carneiro @Johannes Hölzl What would be the proper place for this in mathlib? Somewhere in group_theory?

#### Johan Commelin (Sep 10 2018 at 19:44):

Last updated: May 18 2021 at 16:25 UTC