range_toProd — Mathlib

English

The range of the product-to-prod map toProd equals the set of pairs (l r) of endomaps on A such that for all x,y ∈ A we have r(x) y = x l(y).

Русский

Образ отображения toProd на произведение равен множеству пар (l, r) концевых отображений на A, удовлетворяющих ∀ x,y ∈ A, r(x) y = x l(y).

LaTeX

$$$$ \\operatorname{range}(\\mathrm{toProd}) = \\{ (l,r) \\in (A \\to_L A) \\times (A \\to_L A) \\mid \\forall x,y \\; r(x) \\cdot y = x \\cdot l(y) \\} $$$$

Lean4

theorem range_toProd : Set.range toProd = {lr : (A →L[𝕜] A) × (A →L[𝕜] A) | ∀ x y, lr.2 x * y = x * lr.1 y} :=
  Set.ext fun x =>
    ⟨by
      rintro ⟨a, rfl⟩
      exact a.central, fun hx => ⟨⟨x, hx⟩, rfl⟩⟩

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