map — Mathlib

English

Given a linear map f: M → N, there is an induced linear map map n f: ⋀^n_R M → ⋀^n_R N, defined as the alternating map corresponding to f

Русский

Для линейного отображения f: M → N существует порождаемое отображение map n f: ⋀^n_R M → ⋀^n_R N, задающее соответствие чередующим отображениям.

LaTeX

$$map(n,f) : ⋀^n_R M → ⋀^n_R N$$

Lean4

/-- The linear map between `n`th exterior powers induced by a linear map between the modules. -/
noncomputable def map (f : M →ₗ[R] N) : ⋀[R]^n M →ₗ[R] ⋀[R]^n N :=
  alternatingMapLinearEquiv ((ιMulti R n).compLinearMap f)

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