ιMulti_range — Mathlib

English

The image of ιMulti R n is contained in the nth exterior power: Im(ιMulti_R(n)) ⊆ Λ^n_R M.

Русский

Образ ιMulti R n содержится в n-й внешней степени: Im(ιMulti_R(n)) ⊆ Λ^n_R M.

LaTeX

$$$ \\operatorname{Im}(\\iota\\_{Multi,R}(n)) \\subseteq \\bigwedge^n_R M. $$$

Lean4

/-- The image of `ExteriorAlgebra.ιMulti R n` is contained in the `n`th exterior power. -/
theorem ιMulti_range (n : ℕ) : Set.range (ιMulti R n (M := M)) ⊆ ↑(⋀[R]^n M) :=
  by
  rw [Set.range_subset_iff]
  intro v
  rw [ιMulti_apply]
  apply Submodule.pow_subset_pow
  rw [Set.mem_pow]
  exact ⟨fun i => ⟨ι R (v i), LinearMap.mem_range_self _ _⟩, rfl⟩

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