toDual_symm_eq

Mathlib.Order.Synonym

URI: https://scilib.ai/kg/mathlib#OrderDual.toDual_symm_eq

English

The inverse of toDual equals ofDual: toDual.symm = ofDual.

Русский

Обратная к toDual равна ofDual: toDual.symm = ofDual.

LaTeX

$$$ (@toDual \alpha).\text{symm} = \text{ofDual} $$$

Lean4

@[simp]
theorem toDual_symm_eq : (@toDual α).symm = ofDual :=
  rfl

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

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

Разделы

Аффилиация

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