toRingEquiv_opOp — Mathlib

English

The linear map underlying the opposite-constructed algebra hom equals the composition with the opposite-linear-equivalence.

Русский

Линейное отображение, лежащее в основе противоположного отображения, равно композиции с противоположной линейной эквалентностью.

LaTeX

$$(f.fromOpposite hf).toLinearMap = f.toLinearMap ∘ (opLinearEquiv R (M := A)).symm$$

Lean4

@[simp]
theorem toRingEquiv_opOp : (opOp R A : A ≃+* Aᵐᵒᵖᵐᵒᵖ) = RingEquiv.opOp A :=
  rfl

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