isQuotientMap_coe_coe

Mathlib.Topology.Algebra.Ring.Ideal

URI: https://scilib.ai/kg/mathlib#QuotientRing.isQuotientMap_coe_coe

← MathLib Explorer

English

The map p ↦ (mk N p.1, mk N p.2) from R×R to (R/N)×(R/N) is a quotient map.

Русский

Отображение p ↦ (mk N p.1, mk N p.2) из R×R в (R/N)×(R/N) является факторным отображением.

LaTeX

$$IsQuotientMap (fun p => (mk N p.1, mk N p.2))$$

Lean4

theorem isQuotientMap_coe_coe : IsQuotientMap fun p : R × R => (mk N p.1, mk N p.2) :=
  ((isOpenQuotientMap_mk N).prodMap (isOpenQuotientMap_mk N)).isQuotientMap

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

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

Разделы

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

Аффилиация

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