OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanComparisonSchemes.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous source and target polynomial schemes

The alternating length and the source word are selected from the actual normalized Cartan laws before any good profile sets are imposed.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_source_target_comparison_schemes line 31