lift_of

Mathlib.RingTheory.AdjoinRoot

URI: https://scilib.ai/kg/mathlib#AdjoinRoot.lift_of

English

For x ∈ R, the lift map agrees with i on the embedded copy of R: lift i a h (of f x) = i x.

Русский

Для элементов x ∈ R подъемная карта совпадает с i на вложенной копии R: lift i a h (of f x) = i x.

LaTeX

$$$lift\\ i\\ a\\ h\\ (of\\ f\\ x) = i\\,x$$$

Lean4

@[simp]
theorem lift_of {x : R} : lift i a h x = i x := by rw [← mk_C x, lift_mk, eval₂_C]

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

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

Разделы

Аффилиация

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