lift_self_apply

Mathlib.RingTheory.IsAdjoinRoot

URI: https://scilib.ai/kg/mathlib#IsAdjoinRoot.lift_self_apply

← MathLib Explorer

English

For all x ∈ S, the lifted map applied to x equals x.

Русский

Для любого x ∈ S отображение, полученное путём подъёма, возвращает x.

LaTeX

$$$ h.lift(\\text{algebraMap } R S)\\; h.root\\; h.aeval\\_root\\_self(x) = x $$$

Lean4

@[simp]
theorem lift_self_apply (x : S) : h.lift (algebraMap R S) h.root h.aeval_root_self x = x := by
  rw [← h.map_repr x, lift_map, ← aeval_def, h.aeval_root_eq_map]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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