comp_lift

Mathlib.FieldTheory.IsPerfectClosure

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

English

lift i (f ∘ i) p = f; lift is compatible with precomposition by i when i is p-radical and M is perfect.

Русский

lift совместим с предобразом по i: lift i (f ∘ i) p = f при условии, что i p-радикал и M совершенная.

LaTeX

$$lift i (f ∘ i) p = f$$

Lean4

@[simp]
theorem comp_lift : lift i (f.comp i) p = f :=
  IsPRadical.injective_comp_of_perfect _ i p (lift_comp i _ p)

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

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

Разделы

Аффилиация

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