symm_toLexLinearEquiv

Mathlib.Algebra.Order.Module.Equiv

URI: https://scilib.ai/kg/mathlib#symm_toLexLinearEquiv

English

The inverse of toLexLinearEquiv is ofLexLinearEquiv.

Русский

Обратное отображение к toLexLinearEquiv есть ofLexLinearEquiv.

LaTeX

$$$\bigl(toLexLinearEquiv_{\alpha\beta}\bigr)^{-1} = \mathrm{ofLexLinearEquiv}_{\alpha\beta}$$$

Lean4

@[simp]
theorem symm_toLexLinearEquiv : (toLexLinearEquiv α β).symm = ofLexLinearEquiv α β :=
  rfl

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

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

Разделы

Аффилиация

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