exteriorPower — Mathlib

English

The nth exterior power of an R-module M is defined as the range of the nth power of the canonical map iota: M → ExteriorAlgebra R M.

Русский

n-я внешняя степень модуля M определяется как образ n-й степени канонического отображения iota: M → ExteriorAlgebra R M.

LaTeX

$$exteriorPower : Submodule R (ExteriorAlgebra R M) := LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n$$

Lean4

/-- Definition of the `n`th exterior power of a `R`-module `N`. We introduce the notation
`⋀[R]^n M` for `exteriorPower R n M`. -/
abbrev exteriorPower : Submodule R (ExteriorAlgebra R M) :=
  LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n

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