map_symm

Mathlib.LinearAlgebra.Orientation

URI: https://scilib.ai/kg/mathlib#Orientation.map_symm

English

The map of a morphism's inverse is the inverse map.

Русский

Обращение к обратному отображению даёт обратное отображение.

LaTeX

$$$\text{map_symm}: (Orientation.map ι e).symm = Orientation.map ι e.symm.$$$

Lean4

@[simp]
theorem map_symm (e : M ≃ₗ[R] N) : (Orientation.map ι e).symm = Orientation.map ι e.symm :=
  rfl

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

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

Разделы

Аффилиация

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