equiv_comp_apply

Mathlib.FieldTheory.IsPerfectClosure

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

English

For x in K, equiv i j p (i x) = j x.

Русский

Для x в K, equiv i j p (i x) = j x.

LaTeX

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

Lean4

@[simp]
theorem equiv_comp_apply (x : K) : equiv i j p (i x) = j x :=
  PerfectRing.lift_comp_apply i j p x

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

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

Разделы

Аффилиация

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