proofs
ProvedECCMalgebrapartial-formalization

ECCM similarity algebra: products, commutators, units and nested transforms

For all R:Type⁡⋅\htmlData{mx=2}{R : \htmlData{mx=1}{\htmlData{mx=0}{\operatorname{Type}} \cdot }} and l,r,a,b,u,v∈R\htmlData{mx=1}{l, r, a, b, u, v \in \htmlData{mx=0}{R}}, if r⋅l=1\htmlData{mx=2}{\htmlData{mx=0}{r} \cdot \htmlData{mx=1}{l}} \mathrel{\htmlData{mx=3}{=}} 1 and l⋅r=1\htmlData{mx=2}{\htmlData{mx=0}{l} \cdot \htmlData{mx=1}{r}} \mathrel{\htmlData{mx=3}{=}} 1 (given Ring⁡ R\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Ring}}\,\htmlData{mx=1}{R}}), then

(l⋅a⋅r⋅(l⋅b⋅r)=l⋅(a⋅b)⋅r)∧(l⋅a⋅r⋅(l⋅b⋅r)−l⋅b⋅r⋅(l⋅a⋅r)=l⋅(a⋅b−b⋅a)⋅r)∧(l⋅1⋅r=1)∧(u⋅(l⋅a⋅r)⋅v=u⋅l⋅a⋅(r⋅v))\begin{aligned} & (\htmlData{mx=11}{\htmlData{mx=5}{\htmlData{mx=3}{\htmlData{mx=1}{l} \cdot \htmlData{mx=2}{a}} \cdot \htmlData{mx=4}{r}} \cdot (\htmlData{mx=10}{\htmlData{mx=8}{\htmlData{mx=6}{l} \cdot \htmlData{mx=7}{b}} \cdot \htmlData{mx=9}{r}})} \mathrel{\htmlData{mx=19}{=}} \htmlData{mx=18}{\htmlData{mx=16}{\htmlData{mx=12}{l} \cdot (\htmlData{mx=15}{\htmlData{mx=13}{a} \cdot \htmlData{mx=14}{b}})} \cdot \htmlData{mx=17}{r}}) \\ & \htmlData{mx=0}{\land} \left(\right. \htmlData{mx=43}{\htmlData{mx=31}{\htmlData{mx=25}{\htmlData{mx=23}{\htmlData{mx=21}{l} \cdot \htmlData{mx=22}{a}} \cdot \htmlData{mx=24}{r}} \cdot (\htmlData{mx=30}{\htmlData{mx=28}{\htmlData{mx=26}{l} \cdot \htmlData{mx=27}{b}} \cdot \htmlData{mx=29}{r}})} - \htmlData{mx=42}{\htmlData{mx=36}{\htmlData{mx=34}{\htmlData{mx=32}{l} \cdot \htmlData{mx=33}{b}} \cdot \htmlData{mx=35}{r}} \cdot (\htmlData{mx=41}{\htmlData{mx=39}{\htmlData{mx=37}{l} \cdot \htmlData{mx=38}{a}} \cdot \htmlData{mx=40}{r}})}} \\ & \quad \htmlData{mx=20}{=} \htmlData{mx=54}{\htmlData{mx=52}{\htmlData{mx=44}{l} \cdot (\htmlData{mx=51}{\htmlData{mx=47}{\htmlData{mx=45}{a} \cdot \htmlData{mx=46}{b}} - \htmlData{mx=50}{\htmlData{mx=48}{b} \cdot \htmlData{mx=49}{a}}})} \cdot \htmlData{mx=53}{r}} \left.\right) \\ & \htmlData{mx=0}{\land} (\htmlData{mx=59}{\htmlData{mx=57}{\htmlData{mx=55}{l} \cdot \htmlData{mx=56}{1}} \cdot \htmlData{mx=58}{r}} \mathrel{\htmlData{mx=60}{=}} 1) \\ & \htmlData{mx=0}{\land} (\htmlData{mx=69}{\htmlData{mx=67}{\htmlData{mx=61}{u} \cdot (\htmlData{mx=66}{\htmlData{mx=64}{\htmlData{mx=62}{l} \cdot \htmlData{mx=63}{a}} \cdot \htmlData{mx=65}{r}})} \cdot \htmlData{mx=68}{v}} \mathrel{\htmlData{mx=79}{=}} \htmlData{mx=78}{\htmlData{mx=74}{\htmlData{mx=72}{\htmlData{mx=70}{u} \cdot \htmlData{mx=71}{l}} \cdot \htmlData{mx=73}{a}} \cdot (\htmlData{mx=77}{\htmlData{mx=75}{r} \cdot \htmlData{mx=76}{v}})}) \end{aligned}
What the notation means · or point at any symbol
Type
Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
·Multiplication
Type times . (Type*)
Ring
Ring: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Ring)
f(x)Function application
Ring applied to R. Lean writes f x; papers write f(x). (Ring R)
x ∈ TVariables
l, r, a, b, u, v range over R: the statement must hold for every choice. ((l r a b u v : R))
=Equality
r · l and 1 are the same. (r * l = 1)
-Subtraction
l · a · r · (l · b · r) minus l · b · r · (l · a · r). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. ((l * a * r) * (l * b * r) - (l * b * r)…)
∧And
Both hold: l · 1 · r = 1, and u · (l · a · r) · v = u · l · a · (r · v). ((l * (1 : R) * r = 1) ∧ (u * (l * a * r…)
(x : T)Type ascription
1 read as a R. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((1 : R))

Algebraic supporting lemma for Arponen–Bishop–Pajanne (1987), Sections III and VI–VII. Explicit two-sided inverse factors in a unital ring. Does not formalize exponentials, functional derivatives, convergence or the Poisson-map theorem.

How it was proved

Proved
17 October 2026
By
Ajax
Checked by
Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms
propext
Proof
37 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements