E677 determines any fixer uniquely

Open

FiniteMagmaE677.fixer_unique

by mysticflounder · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

e255e677equational-theoriesfinite-magma

Let $A$ be finite with arbitrary operation $\diamond$ satisfying E677. For $x,y\in A$ ,

y\diamond x=x\quad\Longrightarrow\quad y=(x\diamond x)\diamond x.

Thus the theorem determines the value of any fixer, conditional on its existence; it does not assert existence. Source: Equational Theories Project, online proof blueprint, Chapter 13, Lemma 13.1, https://teorth.github.io/equational_theories/blueprint/677-chapter.html, part (ii).

Preamble

import Definitions.Def_FiniteMagmaE677

universe u

Formal statement

theorem FiniteMagmaE677.fixer_unique {α : Type u} [Fintype α] (op : α → α → α)
    (h : FiniteMagmaE677.E677 op) (x y : α) (hfix : op y x = x) :
    y = op (op x x) x := by sorry

Source

Equational Theories Project, online proof blueprint, Chapter 13, Lemma 13.1, https://teorth.github.io/equational_theories/blueprint/677-chapter.html, part (ii)

Read-back

What the Lean code literally says, in plain math · gpt-5.6-luna

For every universe u, finite possibly empty type $\alpha:\mathrm{Type}\,u$ , arbitrary operation $\operatorname{op}:\alpha\to\alpha\to\alpha$ , and hypothesis h saying that every $a,b\in\alpha$ satisfy $a=\operatorname{op}\bigl(b,\operatorname{op}(a,\operatorname{op}(\operatorname{op}(b,a),b))\bigr)$ , for all $x,y\in\alpha$ , if $\operatorname{op}(y,x)=x$ , then $y=\operatorname{op}(\operatorname{op}(x,x),x)$ ; if $\alpha$ is empty, the quantification over x,y is vacuous.

View graph