toProdMulOpposite_injective — Mathlib

English

The map toProdMulOpposite is injective: if a and b have the same toProdMulOpposite image, then a = b.

Русский

Отображение toProdMulOpposite ин'єктивно: если a и b имеют одинаковое изображение, то a = b.

LaTeX

$$$\\forall a,b \\in \\mathcal{M}(\\mathbb{K},A),\\; \\mathrm{toProdMulOpposite}(a) = \\mathrm{toProdMulOpposite}(b) \\Rightarrow a = b$$$

Lean4

theorem toProdMulOpposite_injective : Function.Injective (toProdMulOpposite : 𝓜(𝕜, A) → (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ) :=
  fun _a _b h =>
  let h' := Prod.ext_iff.mp h
  ext (𝕜 := 𝕜) (A := A) _ _ <| Prod.ext h'.1 <| MulOpposite.op_injective h'.2

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