instCommRingCliffordAlgebraUnitOfNatQuadraticForm

English

For CliffordAlgebra over zero form on Unit, reverse is the identity: x.reverse = x.

Русский

Для CliffordAlgebra с нулевой формой на единице обратное преобразование совпадает с тождественным: x.reverse = x.

LaTeX

$$$\forall x \in \mathrm{CliffordAlgebra}(0),\; x.reverse = x$$$

Lean4

/-- Since the vector space is empty the ring is commutative. -/
instance : CommRing (CliffordAlgebra (0 : QuadraticForm R Unit)) where
  mul_comm := fun x y => by
    induction x using CliffordAlgebra.induction with
    | algebraMap r => apply Algebra.commutes
    | ι x => simp
    | add x₁ x₂ hx₁ hx₂ => rw [mul_add, add_mul, hx₁, hx₂]
    | mul x₁ x₂ hx₁ hx₂ => rw [mul_assoc, hx₂, ← mul_assoc, hx₁, ← mul_assoc]

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