linearEquiv_smul_eq_map — Mathlib

English

For any linear equivalence e: M ≃ₗ[R] M, the action of e on a ray v coincides with applying the ray-map induced by e. In symbols, e • v = Map_e(v).

Русский

Для любого линейного равноотображения e: M ≃ₗ[R] M действие e на луч v совпадает с применением отображения луча, индуцированного e. Обозначим: e • v = map_e(v).

LaTeX

$$$e\cdot v = \mathrm{Module.Ray.map}(e)\,v.$$$

Lean4

/-- The action via `LinearEquiv.apply_distribMulAction` corresponds to `Module.Ray.map`. -/
@[simp]
theorem linearEquiv_smul_eq_map (e : M ≃ₗ[R] M) (v : Module.Ray R M) : e • v = Module.Ray.map e v :=
  rfl

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