flip_flip

Mathlib.LinearAlgebra.PerfectPairing.Basic

URI: https://scilib.ai/kg/mathlib#PerfectPairing.flip_flip

English

The linear isomorphism from M to Dual_R N induced by a perfect pairing is p.toDualLeft: M ≃ₗ[R] Dual R N.

Русский

Линейное изоморфизмирование M к Dual_R N, индуцированное совершенной парой: p.toDualLeft: M ≃ₗ[R] Dual R N.

LaTeX

$$$M \cong_R \operatorname{Dual} R N$$$

Lean4

@[deprecated "No replacement" (since := "2025-05-27")]
theorem flip_flip : p.flip.flip = p :=
  rfl

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

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

Разделы

Аффилиация

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