English
Let X carry two unital binary operations m1 and m2 with units e1 and e2, and suppose they distribute over each other in the Eckmann–Hilton sense. Then the two unit elements coincide, i.e. e1 = e2.
Русский
Пусть X имеет две единичные бинарные операции m1 и m2 с единицами e1 и e2, и они взаимно распределяются по закону Эккманна–Хильтона. Тогда единицы совпадают: e1 = e2.
LaTeX
$$$e_1 = e_2$$$
Lean4
/-- If a type carries two unital binary operations that distribute over each other,
then they have the same unit elements.
In fact, the two operations are the same, and give a commutative monoid structure,
see `eckmann_hilton.CommMonoid`. -/
theorem one : e₁ = e₂ := by simpa only [h₁.left_id, h₁.right_id, h₂.left_id, h₂.right_id] using distrib e₂ e₁ e₁ e₂
