feat(group_theory/eckmann_hilton): add Eckmann-Hilton

[jcommelin]

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

For reviewers: code review check list

[johoelzl]

I'm not sure if this is the right way to formalize it.

Especially, using has_mul as some operator, but not writing down * itself. The idea of the has_... classes is usually to use them as symbols, as syntactic type classes. It doesn't make much sense to use them if you don't use the syntax.

What about statingis_unital using the same style as in lean/library/init/algebra/classes.lean:

structure is_unital (α : Type u) (op : α → α → α) (o : out_param α) :
  extends is_left_id α op o, is_right_id α op o

and also add a is_distrib for it?

[jcommelin]

I'm looking into it, but proves are becoming longer and harder.

universe u
variables (X : Type u)

structure is_unital (op : X → X → X) (e : out_param X)
  extends is_left_id X op e, is_right_id X op e.

local notation a `<`m`>` b := m a b

variables {X} {m₁ m₂: X → X → X} {e₁ e₂ : X}
variables (h₁ : is_unital X m₁ e₁) (h₂ : is_unital X m₂ e₂)
variables (distrib : ∀ a b c d, ((a <m₂> b) <m₁> (c <m₂> d)) = ((a <m₁> c) <m₂> (b <m₁> d)))
include h₁ h₂ distrib

lemma one : (e₁ = e₂) :=
by simpa [h₁.left_id, h₂.left_id, h₁.right_id, h₂.right_id] using distrib e₂ e₁ e₁ e₂

It seems very annoying that I have to explicitly write out h₁.left_id, h₂.left_id, h₁.right_id, h₂.right_id in that simpa. Is there a way to avoid that? If so, then I can try the other lemmas myself.