coe_sub'

Mathlib.Topology.Algebra.Module.LinearMap

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.coe_sub'

English

For g1,g2 ∈ M₂ →SL[σ₂₃] M₃ and f ∈ M →SL[σ₁₂] M₂, (g1 − g2) ∘ f = g1 ∘ f − g2 ∘ f.

Русский

Для отображений g1,g2 и f выполняется (g1 − g2) ∘ f = g1 ∘ f − g2 ∘ f.

LaTeX

$$(g1 - g2) ∘ f = g1 ∘ f - g2 ∘ f$$

Lean4

@[simp, norm_cast]
theorem coe_sub' (f g : M →SL[σ₁₂] M₂) : ⇑(f - g) = f - g :=
  rfl

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

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

Разделы

Аффилиация

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