C_mem_lifts

Mathlib.Algebra.Polynomial.Lifts

URI: https://scilib.ai/kg/mathlib#Polynomial.C_mem_lifts

← MathLib Explorer

English

If r ∈ R, then C(f r) lies in lifts f for a ring hom f.

Русский

Если r ∈ R, то C(f r) принадлежит множеству lifts f для произведённогоRingHom f.

LaTeX

$$$ C ( f r ) \\in \\mathrm{lifts} f $$$

Lean4

/-- If `(r : R)`, then `C (f r)` lifts. -/
theorem C_mem_lifts (f : R →+* S) (r : R) : C (f r) ∈ lifts f :=
  ⟨C r, by simp only [coe_mapRingHom, map_C]⟩

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

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

Разделы

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

Аффилиация

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