ιMulti_zero_apply

Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#ExteriorAlgebra.ιMulti_zero_apply

English

When n = 0, the n-fold exterior product is the multiplicative identity; the zero-fold product equals 1 in ExteriorAlgebra_R M.

Русский

Для n = 0 н-сложное внешнее произведение равно единице; нулевое произведение равно 1 в ExteriorAlgebra_R M.

LaTeX

$$$ ιMulti\\_R(0)(v) = 1. $$$

Lean4

@[simp]
theorem ιMulti_zero_apply (v : Fin 0 → M) : ιMulti R 0 v = 1 := by simp [ιMulti]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru