OAI/GroupTheory/PolycyclicRecognition/Analysis/CompactCharacterCertificates.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite positive identities over compact character families

The identities are locally valid in character space. Compact families therefore have finitely many certificates and one positive lower bound for their supports.

  1. theorem OAI.PolycyclicRecognition.isOpen_positiveIdentitySupport line 23
  2. theorem OAI.PolycyclicRecognition.isOpen_finiteCharacterMonoidDirections line 32
  3. theorem OAI.PolycyclicRecognition.compact_positiveIdentity_certificates line 48