range_toProdMulOpposite — Mathlib

English

The same injectivity fact stated in another form: the map toProdMulOppposite is one-to-one.

Русский

Та же самая инъекция: отображение toProdMulOpposite однозначно восстанавливает исходное элемент.

LaTeX

$$$\\mathrm{Injective}(\\mathrm{toProdMulOpposite})$$$

Lean4

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

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