OAI/Geometry/EinsteinFour/AngularClifford.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Quaternion matrix identities for the sixth-moment mixed contraction.

  1. theorem OAI.PositiveEinsteinFour.Angular.quaternionMatrix_transpose line 13
  2. theorem OAI.PositiveEinsteinFour.Angular.quaternionMatrix_anticommutator line 19
  3. theorem OAI.PositiveEinsteinFour.Angular.oppositeMatrix_anticommutator_zero line 28
  4. theorem OAI.PositiveEinsteinFour.Angular.oppositeMatrix_anticommutator_one line 38
  5. theorem OAI.PositiveEinsteinFour.Angular.oppositeMatrix_anticommutator_two line 48
  6. theorem OAI.PositiveEinsteinFour.Angular.oppositeMatrix_anticommutator line 58
  7. theorem OAI.PositiveEinsteinFour.Angular.oppositeMatrix_commute line 66
  8. theorem OAI.PositiveEinsteinFour.Angular.mixingCoefficient_product line 74
  9. theorem OAI.PositiveEinsteinFour.Angular.mixingCoefficient_product_symm line 86

    Source documentation

    The symmetrized product collapses to the scalar Clifford relation.

    theorem mixingCoefficient_product_symm (i j k l : Fin 3) :
    mixingCoefficient i k * mixingCoefficient j l +
      mixingCoefficient j l * mixingCoefficient i k +
      mixingCoefficient j k * mixingCoefficient i l +
      mixingCoefficient i l * mixingCoefficient j k =
        (if i = j then (if k = l then (4 : ℝ) else 0) else 0) • (1 : Mat4) := by
…

    Mentions: OAI.PositiveEinsteinFour.Angular.mixingCoefficient, OAI.PositiveEinsteinFour.Angular.Mat4