ιMulti_apply_coe — Mathlib

English

The coercion of ιMulti matches the exteriorPower incarnation: applying ιMulti to a vector a in Fin n → M yields the same element as the corresponding exteriorPower ιMulti map in the graded setting.

Русский

Приведение к ιMulti совпадает с реализацией exteriorPower.ιMulti: применение к вектору a в Fin n → M даёт тот же элемент, что и соответствующая карта ιMulti в градуированном контексте.

LaTeX

$$$ιMulti R n a = ExteriorAlgebra.ιMulti R n a$$$

Lean4

@[simp]
theorem ιMulti_apply_coe (a : Fin n → M) : ιMulti R n a = ExteriorAlgebra.ιMulti R n a :=
  rfl

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