ext_ring

Mathlib.Topology.Algebra.Module.LinearMap

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

English

If two continuous linear maps over the identity ring agree at 1, they are equal.

Русский

Если два непрерывных линейных отображения над единичным кольцом согласны на 1, они равны.

LaTeX

$$h: f 1 = g 1 ⇒ f = g$$

Lean4

@[ext]
theorem ext_ring [TopologicalSpace R₁] {f g : R₁ →L[R₁] M₁} (h : f 1 = g 1) : f = g :=
  coe_inj.1 <| LinearMap.ext_ring h

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

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

Разделы

Аффилиация

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