English
The generators of the exterior algebra anticommute: ι_R x · ι_R y + ι_R y · ι_R x = 0 for all x,y ∈ M.
Русский
Генераторы внешней алгебры антикомуют: ι_R x · ι_R y + ι_R y · ι_R x = 0 для всех x,y ∈ M.
LaTeX
$$$\iota_R x \cdot \iota_R y + \iota_R y \cdot \iota_R x = 0$$$
Lean4
theorem ι_mul_prod_list {n : ℕ} (f : Fin n → M) (i : Fin n) : (ι R <| f i) * (List.ofFn fun i => ι R <| f i).prod = 0 :=
by
induction n with
| zero => exact i.elim0
| succ n hn =>
rw [List.ofFn_succ, List.prod_cons, ← mul_assoc]
by_cases h : i = 0
· rw [h, ι_sq_zero, zero_mul]
· replace hn := congr_arg (ι R (f 0) * ·) <| hn (fun i => f <| Fin.succ i) (i.pred h)
simp only at hn
rw [Fin.succ_pred, ← mul_assoc, mul_zero] at hn
refine (eq_zero_iff_eq_zero_of_add_eq_zero ?_).mp hn
rw [← add_mul, ι_add_mul_swap, zero_mul]
