ext_ring

Mathlib.Topology.Algebra.Algebra

URI: https://scilib.ai/kg/mathlib#ContinuousAlgHom.ext_ring

← MathLib Explorer

English

Any two continuous R-algebra morphisms from R to A must be equal.

Русский

Любые две непрерывные R-алгебровые отображения из R в A должны совпасть.

LaTeX

$$forall f g : R \\to_A[R] A, f = g$$

Lean4

/-- Any two continuous `R`-algebra morphisms from `R` are equal -/
@[ext (iff := false)]
theorem ext_ring [TopologicalSpace R] {f g : R →A[R] A} : f = g :=
  coe_inj.mp (ext_id _ _ _)

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

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

Разделы

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

Аффилиация

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