sub_apply' — Mathlib

English

Let f and g be continuous semilinear maps from M to M₂ with respect to a ring hom σ₁₂. Then for every x in M, the subtraction (f − g) evaluated at x equals f(x) − g(x).

Русский

Пусть f и g — непрерывные полулинейные отображения M → M₂ с отношением σ₁₂. Тогда для каждого x ∈ M выполнено (f − g)(x) = f(x) − g(x).

LaTeX

$$$((f - g) x) = f x - g x$$$

Lean4

@[simp]
theorem sub_apply' (f g : M →SL[σ₁₂] M₂) (x : M) : ((f : M →ₛₗ[σ₁₂] M₂) - g) x = f x - g x :=
  rfl

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