ι_mul_ι — Mathlib

English

In the Clifford algebra over a one-dimensional space with zero quadratic form, the products of two generators associated to scalars vanish: ι(0) r1 · ι(0) r2 = 0 for all r1, r2 ∈ R.

Русский

В клиффордовой алгебре над одномерным пространством с нулевой квадратичной формой произведение двух генераторов, соответствующих скалярам, равно нулю: ι(0) r1 · ι(0) r2 = 0 для всех r1, r2 ∈ R.

LaTeX

$$$ι\_{0}(r_{1}) · ι\_{0}(r_{2}) = 0$ for all $r_{1}, r_{2} \in R$$$

Lean4

theorem ι_mul_ι (r₁ r₂) : ι (0 : QuadraticForm R R) r₁ * ι (0 : QuadraticForm R R) r₂ = 0 := by
  rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul r₁, ← smul_eq_mul r₂, LinearMap.map_smul, LinearMap.map_smul,
    smul_mul_smul_comm, ι_sq_scalar, QuadraticMap.zero_apply, RingHom.map_zero, smul_zero]

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