OAI/GroupTheory/PolycyclicRecognition/Analysis/CorrelatedAlternatingHaar.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Alternating products of correlated lifted tuples

No independence is required of the retained tuple set. The product rank is a property of the full limiting multiplication map.

  1. theorem OAI.PolycyclicRecognition.correlated_alternating_haar_image line 24