mapEquiv_symm

Mathlib.Algebra.Star.Unitary

URI: https://scilib.ai/kg/mathlib#unitary.mapEquiv_symm

English

The mapEquiv of the inverse is the inverse of mapEquiv.

Русский

MapEquiv от обратного равен обратному MapEquiv.

LaTeX

$$$\\mathrm{mapEquiv}(f^{-1}) = (\\mathrm{mapEquiv}(f))^{-1}$$$

Lean4

@[simp]
theorem mapEquiv_symm (f : R ≃⋆* S) : mapEquiv f.symm = (mapEquiv f).symm :=
  rfl

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

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

Разделы

Аффилиация

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