ι_sq_zero — Mathlib

English

For every m in M, the square of its image under ι in the exterior algebra is zero: ι_R(m) · ι_R(m) = 0.

Русский

Для каждого m в M квадрат образа ι(m) в произведении внешних степеней равен нулю: ι_R(m) ∙ ι_R(m) = 0.

LaTeX

$$$ι_R(m) \wedge ι_R(m) = 0$$$

Lean4

theorem ι_sq_zero (m : M) : GradedAlgebra.ι R M m * GradedAlgebra.ι R M m = 0 :=
  by
  rw [GradedAlgebra.ι_apply, DirectSum.of_mul_of]
  exact DFinsupp.single_eq_zero.mpr (Subtype.ext <| ExteriorAlgebra.ι_sq_zero _)

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