OAI/Geometry/EinsteinFour/FiniteHodgeTraceCancellation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite-dimensional trace cancellation used for a positive Hodge eigenvalue. Its three identities are the exact/coexact differential identities.

  1. theorem OAI.PositiveEinsteinFour.Geometry.finite_hodge_trace_cancel line 11