OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanSupportedTemplateComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The support inequality for a genuine supported neighboring profile pair

The bases, source word, and alternating target product are selected here. Only the actual profile law and geometric input data are supplied.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.supported_affine_templates_support_le line 37