term⋀[_]^_ — Mathlib

English

The exterior power is equal to the nth power of the range of iota.

Русский

Внешняя степень совпадает с n-й степенью образа iota.

LaTeX

$$ExteriorAlgebra.exteriorPower R n M = (LinearMap.range (ExteriorAlgebra.ι R))^n$$

Lean4

@[inherit_doc exteriorPower, term_parser 1000]
public meta def «term⋀[_]^_» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `ExteriorAlgebra.«term⋀[_]^_» 1024
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "⋀[") (ParserDescr.cat✝ `term 0))
        (ParserDescr.symbol✝ "]^"))
      (ParserDescr.cat✝ `term 1023))

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