OAI/Geometry/RCD/Coordinates/RegularTestAlgebra.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Products remain in the dense regular compact test core

  1. theorem OAI.RegularPointCoordinates.product_mem_compactLaplacianCore line 17