liftEquiv_symm_apply

Mathlib.FieldTheory.IsPerfectClosure

URI: https://scilib.ai/kg/mathlib#PerfectRing.liftEquiv_symm_apply

English

The inverse of liftEquiv sends f to f ∘ i.

Русский

Обратное к liftEquiv отправляет f в f ∘ i.

LaTeX

$$(liftEquiv M i p)^{-1} f = f ∘ i$$

Lean4

theorem liftEquiv_symm_apply : (liftEquiv M i p).symm f = f.comp i :=
  rfl

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

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

Разделы

Аффилиация

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