coe_opLinearEquiv_symm_addEquiv — Mathlib

English

Let M be a module over a semiring R. The inverse of the natural op-linear equivalence from M to its opposite M^op coincides with the canonical additive equivalence from M^op to M.

Русский

Пусть M — модуль над кольцом (или полем) R. Обратное линейного отображения, переводящего M в M^{op}, совпадает по значениям с каноническим аддитивным эквивалентом между M^{op} и M.

LaTeX

$$$ ((\mathrm{opLinearEquiv} R : M \simeq_{R} M^{\mathrm{op}}).symm) = \mathrm{opAddEquiv}.symm $$$

Lean4

@[simp]
theorem coe_opLinearEquiv_symm_addEquiv : ((opLinearEquiv R : M ≃ₗ[R] Mᵐᵒᵖ).symm : Mᵐᵒᵖ ≃+ M) = opAddEquiv.symm :=
  rfl

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