OAI/Geometry/EinsteinFour/DirichletEndpointInvertible.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Positive discrete Dirichlet forms have nonsingular Jacobi endpoints.

  1. theorem OAI.PositiveEinsteinFour.Jacobi.jacobi_endpoint_isUnit_of_dirichlet_posDef line 10