instAdd — Mathlib

English

Alternative articulation: the same range description for toProd, emphasizing the equality condition ∀ x,y.

Русский

Альтернативная формулировка: то же описание образа toProd через условие ∀ x,y.

LaTeX

$$$$ \\operatorname{range}(\\mathrm{toProd}) = \\{ (l,r) \\mid \\forall x,y, r(x) \\cdot y = x \\cdot l(y) \\} $$$$

Lean4

instance instAdd : Add 𝓜(𝕜, A) where
  add 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.add_apply, mul_add, add_mul, central] }

Похожие утверждения