localRingHom_to_map

Mathlib.RingTheory.Localization.AtPrime.Basic

URI: https://scilib.ai/kg/mathlib#Localization.localRingHom_to_map

← MathLib Explorer

English

Localization.localRingHom is a local hom.

Русский

Localization.localRingHom — локальное гомоморфизм.

LaTeX

$$$\text{IsLocalHom}(\mathrm{localRingHom}\ I\ J\ f\ hIJ).$$$

Lean4

theorem localRingHom_to_map (J : Ideal P) [J.IsPrime] (f : R →+* P) (hIJ : I = J.comap f) (x : R) :
    localRingHom I J f hIJ (algebraMap _ _ x) = algebraMap _ _ (f x) :=
  map_eq _ _

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

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

Разделы

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

Аффилиация

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