OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanCoupledTargetTuples.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Separated target tuples from the actual coupled source recurrence

Successful parameters survive the passage from the joint source image to good source states and then to separated target tuples.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_coupled_target_tuples line 33