equiv_symm

Mathlib.FieldTheory.IsPerfectClosure

URI: https://scilib.ai/kg/mathlib#IsPerfectClosure.equiv_symm

English

The inverse of the equivalence equals the swapped equivalence: (equiv i j p).symm = equiv j i p.

Русский

Обратное эквивалента равно swapped эквиваленту: (equiv i j p).symm = equiv j i p.

LaTeX

$$$ (\mathrm{equiv}\, i\, j\, p)^{\mathrm{symm}} = \mathrm{equiv}\, j\, i\, p $$$

Lean4

@[simp]
theorem equiv_symm : (equiv i j p).symm = equiv j i p :=
  rfl

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

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

Разделы

Аффилиация

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