OAI/Geometry/EinsteinFour/JacobiCyclicPowers.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Moving the square-root factors in the finite Jacobi perturbation. Only cyclicity of trace is used; curvature matrices are never commuted.

  1. theorem OAI.PositiveEinsteinFour.Jacobi.product_power_succ line 13
  2. theorem OAI.PositiveEinsteinFour.Jacobi.trace_product_powers line 21
  3. theorem OAI.PositiveEinsteinFour.Jacobi.trace_sandwich_powers line 28
  4. theorem OAI.PositiveEinsteinFour.Jacobi.det_one_sub_sandwich line 32