compRight_apply

Mathlib.Algebra.Module.LinearMap.End

URI: https://scilib.ai/kg/mathlib#LinearMap.compRight_apply

English

Composition on the right distributes over addition: f ∘ (g ⊕ h) = (f ∘ g) ⊕ (f ∘ h).

Русский

Композиция справа распространяется по сложению: f ∘ (g ⊕ h) = (f ∘ g) ⊕ (f ∘ h).

LaTeX

$$f ∘ (g + h) = f ∘ g + f ∘ h$$

Lean4

@[simp]
theorem compRight_apply (f : M₁ →ₗ[R] M₂) (g : M →ₗ[R] M₁) : compRight S f g = f.comp g :=
  rfl

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

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

Разделы

Аффилиация

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