ι_add_mul_swap — Mathlib

English

For a finite family f: Fin n → M and i ∈ Fin n, the product of ι_R(f(i)) with the product of ι_R(f(j)) over j ∈ {0,...,n-1} is zero; i.e., antisymmetrization with a single generator yields zero.

Русский

Для конечного семейства f: Fin n → M и i ∈ Fin n произведение ι_R(f(i)) на произведение ι_R(f(j)) по всем j равно нулю; т.е. антисимметричность с участием одного генератора приводит к нулю.

LaTeX

$$$\iota_R(f(i)) \cdot \prod_{j=0}^{n-1} \iota_R(f(j)) = 0$$$

Lean4

@[simp]
theorem ι_add_mul_swap (x y : M) : ι R x * ι R y + ι R y * ι R x = 0 :=
  CliffordAlgebra.ι_mul_ι_add_swap_of_isOrtho <| .all _ _

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