opLinearEquiv_toAddEquiv

Mathlib.Algebra.Module.Equiv.Opposite

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

English

The toAddEquiv component of opLinearEquiv is equal to opAddEquiv.

Русский

Компонента toAddEquiv у opLinearEquiv равна opAddEquiv.

LaTeX

$$opLinearEquiv_toAddEquiv : (opLinearEquiv R).toAddEquiv = opAddEquiv$$

Lean4

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

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

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

Разделы

Аффилиация

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