ι_range_map_map — Mathlib

English

The span of the range of ιMulti R n is equal to the nth exterior power: Submodule.span R (Set.range (ιMulti R n)) = ⋀[R]^n M.

Русский

Образ ιMulti R n образует всю n-ю внешнюю степень как линейная оболочка: Submodule.span R (Set.range (ιMulti R n)) = ⋀[R]^n M.

LaTeX

$$$ \\operatorname{span}_R(\\operatorname{range}(\\iota\\_{Multi,R}(n))) = \\bigwedge^n_R M. $$$

Lean4

@[simp]
theorem ι_range_map_map (f : M →ₗ[R] N) :
    Submodule.map (AlgHom.toLinearMap (map f)) (LinearMap.range (ι R (M := M))) =
      Submodule.map (ι R) (LinearMap.range f) :=
  CliffordAlgebra.ι_range_map_map _

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