of_comp

Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

URI: https://scilib.ai/kg/mathlib#RingHom.isIntegralElem.of_comp

← MathLib Explorer

English

If (g ∘ f) is integral on x, then g is integral on x.

Русский

Если (g ∘ f) интегральна на x, тогда g интегральна на x.

LaTeX

$${x} \\;: \\; (g \\circ f).IsIntegralElem(x) \\Rightarrow g.IsIntegralElem(x)$$

Lean4

theorem of_comp {x : T} (h : (g.comp f).IsIntegralElem x) : g.IsIntegralElem x :=
  let ⟨p, hp, hp'⟩ := h
  ⟨p.map f, hp.map f, by rwa [← eval₂_map] at hp'⟩

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

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

Разделы

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

Аффилиация

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