English
There is a subtraction operation on DoubleCentralizer: for a,b ∈ 𝓜(𝕜,A), define a − b by toProd := a.toProd − b.toProd and central := …, i.e. the central condition is preserved under subtraction.
Русский
Существует операция вычитания на DoubleCentralizer: для a,b ∈ 𝓜(𝕜,A) определить a − b так, чтобы toProd := a.toProd − b.toProd и центральное условие сохранялось.
LaTeX
$$$$ (a - b)^{\\text{toProd}} = a^{\\text{toProd}} - b^{\\text{toProd}} \\quad\\text{and}\\quad \\forall x,y, (a - b)^{\\text{snd}}(x) \\cdot y = x (a - b)^{\\text{fst}}(y). $$$$
Lean4
instance instSub : Sub 𝓜(𝕜, A) where
sub a
b :=
{ toProd := a.toProd - b.toProd
central := fun x y =>
show (a.snd - b.snd) x * y = x * (a.fst - b.fst) y by
simp only [ContinuousLinearMap.sub_apply, _root_.sub_mul, _root_.mul_sub, central] }
