map_smulₛₗ — Mathlib

English

Let e be a continuous linear equivalence with σ12. Then e(c·x) = σ12(c)·e(x) for all c in R1 and x in M1.

Русский

Пусть e — непрерывное линейное эквивалентное отображение с σ12. Тогда для всех c ∈ R1 и x ∈ M1 выполняется e(c·x) = σ12(c)·e(x).

LaTeX

$$$e(c \cdot x) = \sigma_{12}(c) \cdot e(x)$$$

Lean4

@[simp]
theorem map_smulₛₗ (e : M₁ ≃SL[σ₁₂] M₂) (c : R₁) (x : M₁) : e (c • x) = σ₁₂ c • e x :=
  (e : M₁ →SL[σ₁₂] M₂).map_smulₛₗ c x

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