toContinuousAddMonoidHom_sub

Mathlib.Topology.Algebra.Module.LinearMap

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

English

The function-level equality of f − g with the coerced form holds: ⇑(f − g) = f − g.

Русский

Утверждается равенство функций для f − g и его коэрцированного образа.

LaTeX

$$⇑(f - g) = f - g$$

Lean4

@[simp, norm_cast]
theorem toContinuousAddMonoidHom_sub (f g : M →SL[σ₁₂] M₂) : ↑(f - g) = (f - g : ContinuousAddMonoidHom M M₂) :=
  rfl

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

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

Разделы

Аффилиация

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