OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanStationaryTemplateFactor.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual stationary template-volume comparison

The lower count uses independently sampled coordinates of the actual root factor. The upper count uses the image paths in the ambient group. No volume-comparison statement is assumed as an input.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.templateSupport_le_of_stationary_height_factor line 48