opLinearEquiv_symm_toAddEquiv

Mathlib.Algebra.Module.Equiv.Opposite

URI: https://scilib.ai/kg/mathlib#MulOpposite.opLinearEquiv_symm_toAddEquiv

English

The symm.toAddEquiv equals opAddEquiv.symm.

Русский

symm.toAddEquiv равно opAddEquiv.symm.

LaTeX

$$opLinearEquiv_symm_toAddEquiv : (opLinearEquiv R).symm.toAddEquiv = opAddEquiv.symm$$

Lean4

theorem opLinearEquiv_symm_toAddEquiv : (opLinearEquiv R : M ≃ₗ[R] Mᵐᵒᵖ).symm.toAddEquiv = opAddEquiv.symm :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru